author  wenzelm 
Mon, 03 Nov 1997 12:24:13 +0100  
changeset 4091  771b1f6422a8 
parent 3961  6a8996fb7d99 
child 4238  679a233fb206 
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 

3432  6 
Inductive relation "yahalom" for the Yahalom protocol. 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

7 

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

8 
From page 257 of 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

9 
Burrows, Abadi and Needham. A Logic of Authentication. 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

10 
Proc. Royal Soc. 426 (1989) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

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

12 

1995  13 
open Yahalom; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

14 

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

15 
proof_timing:=true; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

16 
HOL_quantifiers := false; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

17 
Pretty.setdepth 25; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

18 

1995  19 

2322  20 
(*A "possibility property": there are traces that reach the end*) 
1995  21 
goal thy 
22 
"!!A B. [ A ~= B; A ~= Server; B ~= Server ] \ 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

23 
\ ==> EX X NB K. EX evs: yahalom. \ 
3465  24 
\ Says A B {X, Crypt K (Nonce NB)} : set evs"; 
1995  25 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

26 
by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

27 
yahalom.YM4) 2); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

28 
by possibility_tac; 
2013  29 
result(); 
1995  30 

31 

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

32 
(**** Inductive proofs about yahalom ****) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

33 

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

34 
(*Nobody sends themselves messages*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

35 
goal thy "!!evs. evs: yahalom ==> ALL A X. Says A A X ~: set evs"; 
2032  36 
by (etac yahalom.induct 1); 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

37 
by (Auto_tac()); 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

38 
qed_spec_mp "not_Says_to_self"; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

39 
Addsimps [not_Says_to_self]; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

40 
AddSEs [not_Says_to_self RSN (2, rev_notE)]; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

41 

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

42 

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

43 
(** For reasoning about the encrypted portion of messages **) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

44 

1995  45 
(*Lets us treat YM4 using a similar argument as for the Fake case.*) 
3465  46 
goal thy "!!evs. Says S A {Crypt (shrK A) Y, X} : set evs ==> \ 
3683  47 
\ X : analz (spies evs)"; 
4091  48 
by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1); 
3683  49 
qed "YM4_analz_spies"; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

50 

3683  51 
bind_thm ("YM4_parts_spies", 
52 
YM4_analz_spies RS (impOfSubs analz_subset_parts)); 

2110  53 

2133  54 
(*Relates to both YM4 and Oops*) 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

55 
goal thy "!!evs. Says S A {Crypt (shrK A) {B,K,NA,NB}, X} : set evs ==> \ 
3683  56 
\ K : parts (spies evs)"; 
4091  57 
by (blast_tac (claset() addSEs partsEs 
3683  58 
addSDs [Says_imp_spies RS parts.Inj]) 1); 
59 
qed "YM4_Key_parts_spies"; 

2110  60 

3683  61 
(*For proving the easier theorems about X ~: parts (spies evs).*) 
62 
fun parts_spies_tac i = 

63 
forward_tac [YM4_Key_parts_spies] (i+6) THEN 

64 
forward_tac [YM4_parts_spies] (i+5) THEN 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

66 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

67 
(*Induction for regularity theorems. If induction formula has the form 
3683  68 
X ~: analz (spies evs) > ... then it shortens the proof by discarding 
69 
needless information about analz (insert X (spies evs)) *) 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

70 
fun parts_induct_tac i = 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

71 
etac yahalom.induct i 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

72 
THEN 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

73 
REPEAT (FIRSTGOAL analz_mono_contra_tac) 
3683  74 
THEN parts_spies_tac i; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

75 

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

76 

3683  77 
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY 
2013  78 
sends messages containing X! **) 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

79 

3683  80 
(*Spy never sees another agent's shared key! (unless it's bad at start)*) 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

81 
goal thy 
3683  82 
"!!evs. evs : yahalom ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

83 
by (parts_induct_tac 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

84 
by (Fake_parts_insert_tac 1); 
3961  85 
by (ALLGOALS Blast_tac); 
2133  86 
qed "Spy_see_shrK"; 
87 
Addsimps [Spy_see_shrK]; 

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

88 

2133  89 
goal thy 
3683  90 
"!!evs. evs : yahalom ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; 
4091  91 
by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); 
2133  92 
qed "Spy_analz_shrK"; 
93 
Addsimps [Spy_analz_shrK]; 

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

94 

3683  95 
goal thy "!!A. [ Key (shrK A) : parts (spies evs); \ 
96 
\ evs : yahalom ] ==> A:bad"; 

4091  97 
by (blast_tac (claset() addDs [Spy_see_shrK]) 1); 
2133  98 
qed "Spy_see_shrK_D"; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

99 

2133  100 
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); 
101 
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; 

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

102 

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

103 

3432  104 
(*Nobody can have used nonexistent keys! Needed to apply analz_insert_Key*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

105 
goal thy "!!evs. evs : yahalom ==> \ 
3683  106 
\ Key K ~: used evs > K ~: keysFor (parts (spies evs))"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

107 
by (parts_induct_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

108 
(*Fake*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

109 
by (best_tac 
4091  110 
(claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)] 
3961  111 
addIs [impOfSubs analz_subset_parts] 
112 
addDs [impOfSubs (analz_subset_parts RS keysFor_mono)] 

4091  113 
addss (simpset())) 1); 
3961  114 
(*YM24: Because Key K is not fresh, etc.*) 
4091  115 
by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1)); 
2160  116 
qed_spec_mp "new_keys_not_used"; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

117 

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

118 
bind_thm ("new_keys_not_analzd", 
2032  119 
[analz_subset_parts RS keysFor_mono, 
120 
new_keys_not_used] MRS contra_subsetD); 

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

121 

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

122 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

123 

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

124 

2133  125 
(*Describes the form of K when the Server sends this message. Useful for 
126 
Oops as well as main secrecy property.*) 

2110  127 
goal thy 
3501
4ab477ffb4c6
Changed some variables of type msg to lower case (e.g. from NB to nb
paulson
parents:
3466
diff
changeset

128 
"!!evs. [ Says Server A {Crypt (shrK A) {Agent B, Key K, na, nb}, X} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

129 
\ : set evs; \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

130 
\ evs : yahalom ] \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

131 
\ ==> K ~: range shrK"; 
2133  132 
by (etac rev_mp 1); 
133 
by (etac yahalom.induct 1); 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

134 
by (ALLGOALS Asm_simp_tac); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

135 
by (Blast_tac 1); 
2133  136 
qed "Says_Server_message_form"; 
2110  137 

138 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

139 
(*For proofs involving analz.*) 
3683  140 
val analz_spies_tac = 
141 
forward_tac [YM4_analz_spies] 6 THEN 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

142 
forward_tac [Says_Server_message_form] 7 THEN 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

143 
assume_tac 7 THEN REPEAT ((etac exE ORELSE' hyp_subst_tac) 7); 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

144 

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

145 

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

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

147 
The following is to prove theorems of the form 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

148 

3683  149 
Key K : analz (insert (Key KAB) (spies evs)) ==> 
150 
Key K : analz (spies evs) 

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

151 

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

152 
A more general formula must be proved inductively. 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

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

154 

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

155 
(** Session keys are not used to encrypt other session keys **) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

156 

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

157 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

158 
"!!evs. evs : yahalom ==> \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

159 
\ ALL K KK. KK <= Compl (range shrK) > \ 
3683  160 
\ (Key K : analz (Key``KK Un (spies evs))) = \ 
161 
\ (K : KK  Key K : analz (spies evs))"; 

2032  162 
by (etac yahalom.induct 1); 
3683  163 
by analz_spies_tac; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

164 
by (REPEAT_FIRST (resolve_tac [allI, impI])); 
3679  165 
by (REPEAT_FIRST (rtac analz_image_freshK_lemma)); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

166 
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

167 
(*Fake*) 
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

168 
by (spy_analz_tac 2); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

169 
(*Base*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

170 
by (Blast_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

171 
qed_spec_mp "analz_image_freshK"; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

172 

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

173 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

174 
"!!evs. [ evs : yahalom; KAB ~: range shrK ] ==> \ 
3683  175 
\ Key K : analz (insert (Key KAB) (spies evs)) = \ 
176 
\ (K = KAB  Key K : analz (spies evs))"; 

2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

177 
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

178 
qed "analz_insert_freshK"; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

179 

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

180 

2110  181 
(*** The Key K uniquely identifies the Server's message. **) 
182 

183 
goal thy 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

184 
"!!evs. evs : yahalom ==> \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

185 
\ EX A' B' na' nb' X'. ALL A B na nb X. \ 
2110  186 
\ Says Server A \ 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

187 
\ {Crypt (shrK A) {Agent B, Key K, na, nb}, X} \ 
3465  188 
\ : set evs > A=A' & B=B' & na=na' & nb=nb' & X=X'"; 
2110  189 
by (etac yahalom.induct 1); 
4091  190 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 
3708  191 
by (ALLGOALS Clarify_tac); 
2133  192 
by (ex_strip_tac 2); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

193 
by (Blast_tac 2); 
2110  194 
(*Remaining case: YM3*) 
195 
by (expand_case_tac "K = ?y" 1); 

196 
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); 

2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

197 
(*...we assume X is a recent message and handle this case by contradiction*) 
4091  198 
by (blast_tac (claset() addSEs spies_partsEs 
3708  199 
delrules [conjI] (*no splitup to 4 subgoals*)) 1); 
2110  200 
val lemma = result(); 
201 

202 
goal thy 

3683  203 
"!!evs. [ Says Server A \ 
204 
\ {Crypt (shrK A) {Agent B, Key K, na, nb}, X} : set evs; \ 

205 
\ Says Server A' \ 

206 
\ {Crypt (shrK A') {Agent B', Key K, na', nb'}, X'} : set evs; \ 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

207 
\ evs : yahalom ] \ 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

208 
\ ==> A=A' & B=B' & na=na' & nb=nb'"; 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2377
diff
changeset

209 
by (prove_unique_tac lemma 1); 
2110  210 
qed "unique_session_keys"; 
211 

212 

213 
(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **) 

2013  214 

215 
goal thy 

3683  216 
"!!evs. [ A ~: bad; B ~: bad; evs : yahalom ] \ 
2051  217 
\ ==> Says Server A \ 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

218 
\ {Crypt (shrK A) {Agent B, Key K, na, nb}, \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

219 
\ Crypt (shrK B) {Agent A, Key K}} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

220 
\ : set evs > \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

221 
\ Says A Spy {na, nb, Key K} ~: set evs > \ 
3683  222 
\ Key K ~: analz (spies evs)"; 
2032  223 
by (etac yahalom.induct 1); 
3683  224 
by analz_spies_tac; 
2013  225 
by (ALLGOALS 
226 
(asm_simp_tac 

4091  227 
(simpset() addsimps (expand_ifs@pushes) 
3961  228 
addsimps [analz_insert_eq, analz_insert_freshK]))); 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

229 
(*Oops*) 
4091  230 
by (blast_tac (claset() addDs [unique_session_keys]) 3); 
2013  231 
(*YM3*) 
4091  232 
by (blast_tac (claset() delrules [impCE] 
3683  233 
addSEs spies_partsEs 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

234 
addIs [impOfSubs analz_subset_parts]) 2); 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

235 
(*Fake*) 
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

236 
by (spy_analz_tac 1); 
2110  237 
val lemma = result() RS mp RS mp RSN(2,rev_notE); 
2013  238 

239 

3432  240 
(*Final version*) 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

241 
goal thy 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

242 
"!!evs. [ Says Server A \ 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

243 
\ {Crypt (shrK A) {Agent B, Key K, na, nb}, \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

244 
\ Crypt (shrK B) {Agent A, Key K}} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

245 
\ : set evs; \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

246 
\ Says A Spy {na, nb, Key K} ~: set evs; \ 
3683  247 
\ A ~: bad; B ~: bad; evs : yahalom ] \ 
248 
\ ==> Key K ~: analz (spies evs)"; 

2013  249 
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); 
4091  250 
by (blast_tac (claset() addSEs [lemma]) 1); 
2032  251 
qed "Spy_not_see_encrypted_key"; 
2001  252 

253 

3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

254 
(** Security Guarantee for A upon receiving YM3 **) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

255 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

256 
(*If the encrypted message appears then it originated with the Server*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

257 
goal thy 
3683  258 
"!!evs. [ Crypt (shrK A) {Agent B, Key K, na, nb} : parts (spies evs); \ 
259 
\ A ~: bad; evs : yahalom ] \ 

3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

260 
\ ==> Says Server A \ 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

261 
\ {Crypt (shrK A) {Agent B, Key K, na, nb}, \ 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

262 
\ Crypt (shrK B) {Agent A, Key K}} \ 
3465  263 
\ : set evs"; 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

264 
by (etac rev_mp 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

265 
by (parts_induct_tac 1); 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

266 
by (Fake_parts_insert_tac 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

267 
qed "A_trusts_YM3"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

268 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

269 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

270 
(** Security Guarantees for B upon receiving YM4 **) 
2013  271 

2110  272 
(*B knows, by the first part of A's message, that the Server distributed 
273 
the key for A and B. But this part says nothing about nonces.*) 

2001  274 
goal thy 
3683  275 
"!!evs. [ Crypt (shrK B) {Agent A, Key K} : parts (spies evs); \ 
276 
\ B ~: bad; evs : yahalom ] \ 

2001  277 
\ ==> EX NA NB. Says Server A \ 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2377
diff
changeset

278 
\ {Crypt (shrK A) {Agent B, Key K, \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

279 
\ Nonce NA, Nonce NB}, \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

280 
\ Crypt (shrK B) {Agent A, Key K}} \ 
3465  281 
\ : set evs"; 
2032  282 
by (etac rev_mp 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

283 
by (parts_induct_tac 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

284 
by (Fake_parts_insert_tac 1); 
2110  285 
(*YM3*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

286 
by (Blast_tac 1); 
2110  287 
qed "B_trusts_YM4_shrK"; 
288 

3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

289 
(*B knows, by the second part of A's message, that the Server distributed 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

290 
the key quoting nonce NB. This part says nothing about agent names. 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

291 
Secrecy of NB is crucial.*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

292 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

293 
"!!evs. evs : yahalom \ 
3683  294 
\ ==> Nonce NB ~: analz (spies evs) > \ 
295 
\ Crypt K (Nonce NB) : parts (spies evs) > \ 

3543  296 
\ (EX A B NA. Says Server A \ 
297 
\ {Crypt (shrK A) {Agent B, Key K, \ 

298 
\ Nonce NA, Nonce NB}, \ 

299 
\ Crypt (shrK B) {Agent A, Key K}} \ 

3465  300 
\ : set evs)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

301 
by (parts_induct_tac 1); 
3708  302 
by (ALLGOALS Clarify_tac); 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

303 
(*YM3 & Fake*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

304 
by (Blast_tac 2); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

305 
by (Fake_parts_insert_tac 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

306 
(*YM4*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

307 
(*A is uncompromised because NB is secure*) 
3683  308 
by (not_bad_tac "A" 1); 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

309 
(*A's certificate guarantees the existence of the Server message*) 
4091  310 
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

311 
A_trusts_YM3]) 1); 
3464
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

312 
bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp)); 
2133  313 

3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

314 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

315 
(**** Towards proving secrecy of Nonce NB ****) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

316 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

317 
(** Lemmas about the predicate KeyWithNonce **) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

318 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

319 
goalw thy [KeyWithNonce_def] 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

320 
"!!evs. Says Server A \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

321 
\ {Crypt (shrK A) {Agent B, Key K, na, Nonce NB}, X} \ 
3465  322 
\ : set evs ==> KeyWithNonce K NB evs"; 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

323 
by (Blast_tac 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

324 
qed "KeyWithNonceI"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

325 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

326 
goalw thy [KeyWithNonce_def] 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

327 
"KeyWithNonce K NB (Says S A X # evs) = \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

328 
\ (Server = S & \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

329 
\ (EX B n X'. X = {Crypt (shrK A) {Agent B, Key K, n, Nonce NB}, X'}) \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

330 
\  KeyWithNonce K NB evs)"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

331 
by (Simp_tac 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

332 
by (Blast_tac 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

333 
qed "KeyWithNonce_Says"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

334 
Addsimps [KeyWithNonce_Says]; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

335 

3464
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

336 
(*A fresh key cannot be associated with any nonce 
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

337 
(with respect to a given trace). *) 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

338 
goalw thy [KeyWithNonce_def] 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

339 
"!!evs. Key K ~: used evs ==> ~ KeyWithNonce K NB evs"; 
4091  340 
by (blast_tac (claset() addSEs spies_partsEs) 1); 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

341 
qed "fresh_not_KeyWithNonce"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

342 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

343 
(*The Server message associates K with NB' and therefore not with any 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

344 
other nonce NB.*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

345 
goalw thy [KeyWithNonce_def] 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

346 
"!!evs. [ Says Server A \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

347 
\ {Crypt (shrK A) {Agent B, Key K, na, Nonce NB'}, X} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

348 
\ : set evs; \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

349 
\ NB ~= NB'; evs : yahalom ] \ 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

350 
\ ==> ~ KeyWithNonce K NB evs"; 
4091  351 
by (blast_tac (claset() addDs [unique_session_keys]) 1); 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

352 
qed "Says_Server_KeyWithNonce"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

353 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

354 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

355 
(*The only nonces that can be found with the help of session keys are 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

356 
those distributed as nonce NB by the Server. The form of the theorem 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

357 
recalls analz_image_freshK, but it is much more complicated.*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

358 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

359 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

360 
(*As with analz_image_freshK, we take some pains to express the property 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

361 
as a logical equivalence so that the simplifier can apply it.*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

362 
goal thy 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

363 
"!!evs. P > (X : analz (G Un H)) > (X : analz H) ==> \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

364 
\ P > (X : analz (G Un H)) = (X : analz H)"; 
4091  365 
by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1); 
3961  366 
val Nonce_secrecy_lemma = result(); 
2133  367 

368 
goal thy 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

369 
"!!evs. evs : yahalom ==> \ 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

370 
\ (ALL KK. KK <= Compl (range shrK) > \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

371 
\ (ALL K: KK. ~ KeyWithNonce K NB evs) > \ 
3683  372 
\ (Nonce NB : analz (Key``KK Un (spies evs))) = \ 
373 
\ (Nonce NB : analz (spies evs)))"; 

3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

374 
by (etac yahalom.induct 1); 
3683  375 
by analz_spies_tac; 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

376 
by (REPEAT_FIRST (resolve_tac [impI RS allI])); 
3961  377 
by (REPEAT_FIRST (rtac Nonce_secrecy_lemma)); 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

378 
(*For Oops, simplification proves NBa~=NB. By Says_Server_KeyWithNonce, 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

379 
we get (~ KeyWithNonce K NB evsa); then simplification can apply the 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

380 
induction hypothesis with KK = {K}.*) 
3961  381 
by (ALLGOALS (*12 seconds*) 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

382 
(asm_simp_tac 
3961  383 
(analz_image_freshK_ss 
384 
addsimps expand_ifs 

385 
addsimps [all_conj_distrib, analz_image_freshK, 

386 
KeyWithNonce_Says, fresh_not_KeyWithNonce, 

387 
imp_disj_not1, (*Moves NBa~=NB to the front*) 

388 
Says_Server_KeyWithNonce]))); 

3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

389 
(*Base*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

390 
by (Blast_tac 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

391 
(*Fake*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

392 
by (spy_analz_tac 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

393 
(*YM4*) (** LEVEL 7 **) 
3683  394 
by (not_bad_tac "A" 1); 
395 
by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1 

3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

396 
THEN REPEAT (assume_tac 1)); 
4091  397 
by (blast_tac (claset() addIs [KeyWithNonceI]) 1); 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

398 
qed_spec_mp "Nonce_secrecy"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

399 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

400 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

401 
(*Version required below: if NB can be decrypted using a session key then it 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

402 
was distributed with that key. The more general form above is required 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

403 
for the induction to carry through.*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

404 
goal thy 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

405 
"!!evs. [ Says Server A \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

406 
\ {Crypt (shrK A) {Agent B, Key KAB, na, Nonce NB'}, X} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

407 
\ : set evs; \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

408 
\ NB ~= NB'; KAB ~: range shrK; evs : yahalom ] \ 
3683  409 
\ ==> (Nonce NB : analz (insert (Key KAB) (spies evs))) = \ 
410 
\ (Nonce NB : analz (spies evs))"; 

3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

411 
by (asm_simp_tac (analz_image_freshK_ss addsimps 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

412 
[Nonce_secrecy, Says_Server_KeyWithNonce]) 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

413 
qed "single_Nonce_secrecy"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

414 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

415 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

416 
(*** The Nonce NB uniquely identifies B's message. ***) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

417 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

418 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

419 
"!!evs. evs : yahalom ==> \ 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

420 
\ EX NA' A' B'. ALL NA A B. \ 
3683  421 
\ Crypt (shrK B) {Agent A, Nonce NA, nb} : parts(spies evs) \ 
422 
\ > B ~: bad > NA = NA' & A = A' & B = B'"; 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

423 
by (parts_induct_tac 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

424 
(*Fake*) 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

425 
by (REPEAT (etac (exI RSN (2,exE)) 1) (*stripping EXs makes proof faster*) 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

426 
THEN Fake_parts_insert_tac 1); 
4091  427 
by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1); 
2133  428 
(*YM2: creation of new Nonce. Move assertion into global context*) 
3501
4ab477ffb4c6
Changed some variables of type msg to lower case (e.g. from NB to nb
paulson
parents:
3466
diff
changeset

429 
by (expand_case_tac "nb = ?y" 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

430 
by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1)); 
4091  431 
by (blast_tac (claset() addSEs spies_partsEs) 1); 
2133  432 
val lemma = result(); 
433 

2110  434 
goal thy 
3683  435 
"!!evs.[ Crypt (shrK B) {Agent A, Nonce NA, nb} : parts (spies evs); \ 
436 
\ Crypt (shrK B') {Agent A', Nonce NA', nb} : parts (spies evs); \ 

437 
\ evs : yahalom; B ~: bad; B' ~: bad ] \ 

2133  438 
\ ==> NA' = NA & A' = A & B' = B"; 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2377
diff
changeset

439 
by (prove_unique_tac lemma 1); 
2133  440 
qed "unique_NB"; 
441 

442 

3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

443 
(*Variant useful for proving secrecy of NB: the Says... form allows 
3683  444 
not_bad_tac to remove the assumption B' ~: bad.*) 
2133  445 
goal thy 
3501
4ab477ffb4c6
Changed some variables of type msg to lower case (e.g. from NB to nb
paulson
parents:
3466
diff
changeset

446 
"!!evs.[ Says C D {X, Crypt (shrK B) {Agent A, Nonce NA, nb}} \ 
3683  447 
\ : set evs; B ~: bad; \ 
3501
4ab477ffb4c6
Changed some variables of type msg to lower case (e.g. from NB to nb
paulson
parents:
3466
diff
changeset

448 
\ Says C' D' {X', Crypt (shrK B') {Agent A', Nonce NA', nb}} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

449 
\ : set evs; \ 
3683  450 
\ nb ~: analz (spies evs); evs : yahalom ] \ 
2133  451 
\ ==> NA' = NA & A' = A & B' = B"; 
3683  452 
by (not_bad_tac "B'" 1); 
4091  453 
by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj] 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

454 
addSEs [MPair_parts] 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

455 
addDs [unique_NB]) 1); 
2133  456 
qed "Says_unique_NB"; 
457 

3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

458 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

459 
(** A nonce value is never used both as NA and as NB **) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

460 

2133  461 
goal thy 
3683  462 
"!!evs. [ B ~: bad; evs : yahalom ] \ 
463 
\ ==> Nonce NB ~: analz (spies evs) > \ 

464 
\ Crypt (shrK B') {Agent A', Nonce NB, nb'} : parts(spies evs) > \ 

465 
\ Crypt (shrK B) {Agent A, Nonce NA, Nonce NB} ~: parts(spies evs)"; 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

466 
by (parts_induct_tac 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

467 
by (Fake_parts_insert_tac 1); 
4091  468 
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj] 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

469 
addSIs [parts_insertI] 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

470 
addSEs partsEs) 1); 
3464
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

471 
bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE)); 
2133  472 

3464
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

473 
(*The Server sends YM3 only in response to YM2.*) 
2133  474 
goal thy 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

475 
"!!evs. [ Says Server A \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

476 
\ {Crypt (shrK A) {Agent B, k, na, nb}, X} : set evs; \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

477 
\ evs : yahalom ] \ 
2133  478 
\ ==> EX B'. Says B' Server \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

479 
\ { Agent B, Crypt (shrK B) {Agent A, na, nb} } \ 
3465  480 
\ : set evs"; 
2133  481 
by (etac rev_mp 1); 
482 
by (etac yahalom.induct 1); 

483 
by (ALLGOALS Asm_simp_tac); 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

484 
by (ALLGOALS Blast_tac); 
2133  485 
qed "Says_Server_imp_YM2"; 
486 

487 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

488 
(*A vital theorem for B, that nonce NB remains secure from the Spy.*) 
2133  489 
goal thy 
3683  490 
"!!evs. [ A ~: bad; B ~: bad; evs : yahalom ] \ 
2133  491 
\ ==> Says B Server \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

492 
\ {Agent B, Crypt (shrK B) {Agent A, Nonce NA, Nonce NB}} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

493 
\ : set evs > \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

494 
\ (ALL k. Says A Spy {Nonce NA, Nonce NB, k} ~: set evs) > \ 
3683  495 
\ Nonce NB ~: analz (spies evs)"; 
2133  496 
by (etac yahalom.induct 1); 
3683  497 
by analz_spies_tac; 
2133  498 
by (ALLGOALS 
499 
(asm_simp_tac 

4091  500 
(simpset() addsimps (expand_ifs@pushes) 
3961  501 
addsimps [analz_insert_eq, analz_insert_freshK]))); 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

502 
(*Prove YM3 by showing that no NB can also be an NA*) 
4091  503 
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj] 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

504 
addSEs [MPair_parts] 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

505 
addDs [no_nonce_YM1_YM2, Says_unique_NB]) 4 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

506 
THEN flexflex_tac); 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

507 
(*YM2: similar freshness reasoning*) 
4091  508 
by (blast_tac (claset() addSEs partsEs 
3683  509 
addDs [Says_imp_spies RS analz.Inj, 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

510 
impOfSubs analz_subset_parts]) 3); 
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

511 
(*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*) 
4091  512 
by (blast_tac (claset() addSIs [parts_insertI] 
3683  513 
addSEs spies_partsEs) 2); 
2377  514 
(*Fake*) 
515 
by (spy_analz_tac 1); 

3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

516 
(** LEVEL 7: YM4 and Oops remain **) 
3708  517 
by (ALLGOALS Clarify_tac); 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

518 
(*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) 
3683  519 
by (not_bad_tac "Aa" 1); 
520 
by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1); 

2133  521 
by (forward_tac [Says_Server_message_form] 3); 
522 
by (forward_tac [Says_Server_imp_YM2] 4); 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

523 
by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE])); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

524 
(* use Says_unique_NB to identify message components: Aa=A, Ba=B, NAa=NA *) 
4091  525 
by (blast_tac (claset() addDs [Says_unique_NB, Spy_not_see_encrypted_key, 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

526 
impOfSubs Fake_analz_insert]) 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

527 
(** LEVEL 14 **) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

528 
(*Oops case: if the nonce is betrayed now, show that the Oops event is 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

529 
covered by the quantified Oops assumption.*) 
4091  530 
by (full_simp_tac (simpset() addsimps [all_conj_distrib]) 1); 
2133  531 
by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1); 
532 
by (expand_case_tac "NB = NBa" 1); 

3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

533 
(*If NB=NBa then all other components of the Oops message agree*) 
4091  534 
by (blast_tac (claset() addDs [Says_unique_NB]) 1 THEN flexflex_tac); 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

535 
(*case NB ~= NBa*) 
4091  536 
by (asm_simp_tac (simpset() addsimps [single_Nonce_secrecy]) 1); 
537 
by (blast_tac (claset() addSEs [MPair_parts] 

3683  538 
addDs [Says_imp_spies RS parts.Inj, 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

539 
no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

540 
bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp)); 
2133  541 

2001  542 

3464
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

543 
(*B's session key guarantee from YM4. The two certificates contribute to a 
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

544 
single conclusion about the Server's message. Note that the "Says A Spy" 
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

545 
assumption must quantify over ALL POSSIBLE keys instead of our particular K. 
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

546 
If this run is broken and the spy substitutes a certificate containing an 
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

547 
old key, B has no means of telling.*) 
2001  548 
goal thy 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

549 
"!!evs. [ Says B Server \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

550 
\ {Agent B, Crypt (shrK B) {Agent A, Nonce NA, Nonce NB}} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

551 
\ : set evs; \ 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

552 
\ Says A' B {Crypt (shrK B) {Agent A, Key K}, \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

553 
\ Crypt K (Nonce NB)} : set evs; \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

554 
\ ALL k. Says A Spy {Nonce NA, Nonce NB, k} ~: set evs; \ 
3683  555 
\ A ~: bad; B ~: bad; evs : yahalom ] \ 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

556 
\ ==> Says Server A \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

557 
\ {Crypt (shrK A) {Agent B, Key K, \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

558 
\ Nonce NA, Nonce NB}, \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

559 
\ Crypt (shrK B) {Agent A, Key K}} \ 
3465  560 
\ : set evs"; 
2133  561 
by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); 
3683  562 
by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1 THEN 
2133  563 
dtac B_trusts_YM4_shrK 1); 
2170  564 
by (dtac B_trusts_YM4_newK 3); 
2110  565 
by (REPEAT_FIRST (eresolve_tac [asm_rl, exE])); 
2133  566 
by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1); 
2170  567 
by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1)); 
4091  568 
by (blast_tac (claset() addDs [Says_unique_NB]) 1); 
2322  569 
qed "B_trusts_YM4"; 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

570 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

571 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

572 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

573 
(*** Authenticating B to A ***) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

574 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

575 
(*The encryption in message YM2 tells us it cannot be faked.*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

576 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

577 
"!!evs. evs : yahalom \ 
3683  578 
\ ==> Crypt (shrK B) {Agent A, Nonce NA, nb} : parts (spies evs) > \ 
579 
\ B ~: bad > \ 

3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

580 
\ Says B Server {Agent B, Crypt (shrK B) {Agent A, Nonce NA, nb}} \ 
3465  581 
\ : set evs"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

582 
by (parts_induct_tac 1); 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

583 
by (Fake_parts_insert_tac 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

584 
bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

585 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

586 
(*If the server sends YM3 then B sent YM2*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

587 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

588 
"!!evs. evs : yahalom \ 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

589 
\ ==> Says Server A {Crypt (shrK A) {Agent B, Key K, Nonce NA, nb}, X} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

590 
\ : set evs > \ 
3683  591 
\ B ~: bad > \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

592 
\ Says B Server {Agent B, Crypt (shrK B) {Agent A, Nonce NA, nb}} \ 
3465  593 
\ : set evs"; 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

594 
by (etac yahalom.induct 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

595 
by (ALLGOALS Asm_simp_tac); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

596 
(*YM4*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

597 
by (Blast_tac 2); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

598 
(*YM3*) 
4091  599 
by (best_tac (claset() addSDs [B_Said_YM2, Says_imp_spies RS parts.Inj] 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

600 
addSEs [MPair_parts]) 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

601 
val lemma = result() RSN (2, rev_mp) RS mp > standard; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

602 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

603 
(*If A receives YM3 then B has used nonce NA (and therefore is alive)*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

604 
goal thy 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

605 
"!!evs. [ Says S A {Crypt (shrK A) {Agent B, Key K, Nonce NA, nb}, X} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

606 
\ : set evs; \ 
3683  607 
\ A ~: bad; B ~: bad; evs : yahalom ] \ 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

608 
\ ==> Says B Server {Agent B, Crypt (shrK B) {Agent A, Nonce NA, nb}} \ 
3465  609 
\ : set evs"; 
4091  610 
by (blast_tac (claset() addSDs [A_trusts_YM3, lemma] 
3683  611 
addEs spies_partsEs) 1); 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

612 
qed "YM3_auth_B_to_A"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

613 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

614 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

615 
(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

616 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

617 
(*Assuming the session key is secure, if both certificates are present then 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

618 
A has said NB. We can't be sure about the rest of A's message, but only 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

619 
NB matters for freshness.*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

620 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

621 
"!!evs. evs : yahalom \ 
3683  622 
\ ==> Key K ~: analz (spies evs) > \ 
623 
\ Crypt K (Nonce NB) : parts (spies evs) > \ 

624 
\ Crypt (shrK B) {Agent A, Key K} : parts (spies evs) > \ 

625 
\ B ~: bad > \ 

626 
\ (EX X. Says A B {X, Crypt K (Nonce NB)} : set evs)"; 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

627 
by (parts_induct_tac 1); 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

628 
(*Fake*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

629 
by (Fake_parts_insert_tac 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

630 
(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*) 
4091  631 
by (fast_tac (claset() addSDs [Crypt_imp_invKey_keysFor] addss (simpset())) 1); 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

632 
(*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*) 
4091  633 
by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1); 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

634 
(*yes: apply unicity of session keys*) 
3683  635 
by (not_bad_tac "Aa" 1); 
4091  636 
by (blast_tac (claset() addSEs [MPair_parts] 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

637 
addSDs [A_trusts_YM3, B_trusts_YM4_shrK] 
3683  638 
addDs [Says_imp_spies RS parts.Inj, 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

639 
unique_session_keys]) 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

640 
val lemma = normalize_thm [RSspec, RSmp] (result()) > standard; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

641 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

642 
(*If B receives YM4 then A has used nonce NB (and therefore is alive). 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

643 
Moreover, A associates K with NB (thus is talking about the same run). 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

644 
Other premises guarantee secrecy of K.*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

645 
goal thy 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

646 
"!!evs. [ Says B Server \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

647 
\ {Agent B, Crypt (shrK B) {Agent A, Nonce NA, Nonce NB}} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

648 
\ : set evs; \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

649 
\ Says A' B {Crypt (shrK B) {Agent A, Key K}, \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

650 
\ Crypt K (Nonce NB)} : set evs; \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

651 
\ (ALL NA k. Says A Spy {Nonce NA, Nonce NB, k} ~: set evs); \ 
3683  652 
\ A ~: bad; B ~: bad; evs : yahalom ] \ 
3465  653 
\ ==> EX X. Says A B {X, Crypt K (Nonce NB)} : set evs"; 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

654 
by (dtac B_trusts_YM4 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

655 
by (REPEAT_FIRST (eresolve_tac [asm_rl, spec])); 
3683  656 
by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1); 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

657 
by (rtac lemma 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

658 
by (rtac Spy_not_see_encrypted_key 2); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

659 
by (REPEAT_FIRST assume_tac); 
4091  660 
by (blast_tac (claset() addSEs [MPair_parts] 
3683  661 
addDs [Says_imp_spies RS parts.Inj]) 1); 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

662 
qed_spec_mp "YM4_imp_A_Said_YM3"; 