author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 9166  74d403974c8d 
child 10833  c0844a30ea4e 
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 

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

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

14 

1995  15 

2322  16 
(*A "possibility property": there are traces that reach the end*) 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

17 
Goal "A ~= Server \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

18 
\ ==> EX X NB K. EX evs: yahalom. \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

19 
\ Says A B {X, Crypt K (Nonce NB)} : set evs"; 
1995  20 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
6335  21 
by (rtac (yahalom.Nil RS 
22 
yahalom.YM1 RS yahalom.Reception RS 

23 
yahalom.YM2 RS yahalom.Reception RS 

24 
yahalom.YM3 RS yahalom.Reception RS yahalom.YM4) 2); 

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

25 
by possibility_tac; 
2013  26 
result(); 
1995  27 

6335  28 
Goal "[ Gets B X : set evs; evs : yahalom ] ==> EX A. Says A B X : set evs"; 
29 
by (etac rev_mp 1); 

30 
by (etac yahalom.induct 1); 

31 
by Auto_tac; 

32 
qed "Gets_imp_Says"; 

33 

34 
(*Must be proved separately for each protocol*) 

35 
Goal "[ Gets B X : set evs; evs : yahalom ] ==> X : knows Spy evs"; 

36 
by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1); 

37 
qed"Gets_imp_knows_Spy"; 

38 
AddDs [Gets_imp_knows_Spy RS parts.Inj]; 

39 

40 
fun g_not_bad_tac s = 

7499  41 
ftac Gets_imp_Says THEN' assume_tac THEN' not_bad_tac s; 
6335  42 

1995  43 

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

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

45 

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

46 

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

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

48 

1995  49 
(*Lets us treat YM4 using a similar argument as for the Fake case.*) 
6335  50 
Goal "[ Gets A {Crypt (shrK A) Y, X} : set evs; evs : yahalom ] \ 
51 
\ ==> X : analz (knows Spy evs)"; 

52 
by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1); 

53 
qed "YM4_analz_knows_Spy"; 

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

54 

6335  55 
bind_thm ("YM4_parts_knows_Spy", 
56 
YM4_analz_knows_Spy RS (impOfSubs analz_subset_parts)); 

2110  57 

6335  58 
(*For Oops*) 
59 
Goal "Says Server A {Crypt (shrK A) {B,K,NA,NB}, X} : set evs \ 

60 
\ ==> K : parts (knows Spy evs)"; 

4091  61 
by (blast_tac (claset() addSEs partsEs 
6335  62 
addSDs [Says_imp_knows_Spy RS parts.Inj]) 1); 
63 
qed "YM4_Key_parts_knows_Spy"; 

2110  64 

6335  65 
(*For proving the easier theorems about X ~: parts (knows Spy evs).*) 
66 
fun parts_knows_Spy_tac i = 

67 
EVERY 

7499  68 
[ftac YM4_Key_parts_knows_Spy (i+7), 
69 
ftac YM4_parts_knows_Spy (i+6), assume_tac (i+6), 

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

71 

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

72 
(*Induction for regularity theorems. If induction formula has the form 
6335  73 
X ~: analz (knows Spy evs) > ... then it shortens the proof by discarding 
74 
needless information about analz (insert X (knows Spy evs)) *) 

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

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

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

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

78 
REPEAT (FIRSTGOAL analz_mono_contra_tac) 
6335  79 
THEN parts_knows_Spy_tac i; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

80 

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

81 

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

84 

3683  85 
(*Spy never sees another agent's shared key! (unless it's bad at start)*) 
6335  86 
Goal "evs : yahalom ==> (Key (shrK A) : parts (knows Spy evs)) = (A : bad)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

88 
by (Fake_parts_insert_tac 1); 
3961  89 
by (ALLGOALS Blast_tac); 
2133  90 
qed "Spy_see_shrK"; 
91 
Addsimps [Spy_see_shrK]; 

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

92 

6335  93 
Goal "evs : yahalom ==> (Key (shrK A) : analz (knows Spy evs)) = (A : bad)"; 
4091  94 
by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); 
2133  95 
qed "Spy_analz_shrK"; 
96 
Addsimps [Spy_analz_shrK]; 

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

97 

4471  98 
AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
99 
Spy_analz_shrK RSN (2, rev_iffD1)]; 

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

100 

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

101 

3432  102 
(*Nobody can have used nonexistent keys! Needed to apply analz_insert_Key*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

103 
Goal "evs : yahalom ==> \ 
6335  104 
\ Key K ~: used evs > K ~: keysFor (parts (knows Spy evs))"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

106 
(*Fake*) 
4509
828148415197
Making proofs faster, especially using keysFor_parts_insert
paulson
parents:
4477
diff
changeset

107 
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); 
3961  108 
(*YM24: Because Key K is not fresh, etc.*) 
6335  109 
by (REPEAT (blast_tac (claset() addSEs knows_Spy_partsEs) 1)); 
2160  110 
qed_spec_mp "new_keys_not_used"; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

111 

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

112 
bind_thm ("new_keys_not_analzd", 
2032  113 
[analz_subset_parts RS keysFor_mono, 
114 
new_keys_not_used] MRS contra_subsetD); 

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

115 

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

116 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 
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 

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

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

121 
Goal "[ Says Server A {Crypt (shrK A) {Agent B, Key K, na, nb}, X} \ 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

122 
\ : set evs; evs : yahalom ] \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

123 
\ ==> K ~: range shrK"; 
2133  124 
by (etac rev_mp 1); 
125 
by (etac yahalom.induct 1); 

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

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

127 
by (Blast_tac 1); 
5073  128 
qed "Says_Server_not_range"; 
129 

130 
Addsimps [Says_Server_not_range]; 

2110  131 

132 

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

133 
(*For proofs involving analz.*) 
6335  134 
val analz_knows_Spy_tac = 
7499  135 
ftac YM4_analz_knows_Spy 7 THEN assume_tac 7; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

136 

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

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

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

139 

6335  140 
Key K : analz (insert (Key KAB) (knows Spy evs)) ==> 
141 
Key K : analz (knows Spy evs) 

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

142 

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

143 
A more general formula must be proved inductively. 
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 
(** Session keys are not used to encrypt other session keys **) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

147 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

148 
Goal "evs : yahalom ==> \ 
5492  149 
\ ALL K KK. KK <=  (range shrK) > \ 
6335  150 
\ (Key K : analz (Key``KK Un (knows Spy evs))) = \ 
151 
\ (K : KK  Key K : analz (knows Spy evs))"; 

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

154 
by (REPEAT_FIRST (resolve_tac [allI, impI])); 
3679  155 
by (REPEAT_FIRST (rtac analz_image_freshK_lemma)); 
5073  156 
by (ALLGOALS (asm_simp_tac 
157 
(analz_image_freshK_ss addsimps [Says_Server_not_range]))); 

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

158 
(*Fake*) 
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4238
diff
changeset

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

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

161 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

162 
Goal "[ evs : yahalom; KAB ~: range shrK ] \ 
6335  163 
\ ==> Key K : analz (insert (Key KAB) (knows Spy evs)) = \ 
164 
\ (K = KAB  Key K : analz (knows Spy evs))"; 

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

165 
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

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

167 

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

168 

2110  169 
(*** The Key K uniquely identifies the Server's message. **) 
170 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

171 
Goal "evs : yahalom ==> \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

172 
\ EX A' B' na' nb' X'. ALL A B na nb X. \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

173 
\ Says Server A \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

174 
\ {Crypt (shrK A) {Agent B, Key K, na, nb}, X} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

175 
\ : set evs > A=A' & B=B' & na=na' & nb=nb' & X=X'"; 
2110  176 
by (etac yahalom.induct 1); 
4091  177 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 
3708  178 
by (ALLGOALS Clarify_tac); 
2133  179 
by (ex_strip_tac 2); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

180 
by (Blast_tac 2); 
2110  181 
(*Remaining case: YM3*) 
182 
by (expand_case_tac "K = ?y" 1); 

183 
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

184 
(*...we assume X is a recent message and handle this case by contradiction*) 
6335  185 
by (blast_tac (claset() addSEs knows_Spy_partsEs 
4238
679a233fb206
Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
paulson
parents:
4091
diff
changeset

186 
delrules [conjI] (*no splitup to 4 subgoals*)) 1); 
2110  187 
val lemma = result(); 
188 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

189 
Goal "[ Says Server A \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

190 
\ {Crypt (shrK A) {Agent B, Key K, na, nb}, X} : set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

191 
\ Says Server A' \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

192 
\ {Crypt (shrK A') {Agent B', Key K, na', nb'}, X'} : set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

193 
\ evs : yahalom ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

195 
by (prove_unique_tac lemma 1); 
2110  196 
qed "unique_session_keys"; 
197 

198 

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

2013  200 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

201 
Goal "[ A ~: bad; B ~: bad; evs : yahalom ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

202 
\ ==> Says Server A \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

203 
\ {Crypt (shrK A) {Agent B, Key K, na, nb}, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

204 
\ Crypt (shrK B) {Agent A, Key K}} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

205 
\ : set evs > \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

206 
\ Notes Spy {na, nb, Key K} ~: set evs > \ 
6335  207 
\ Key K ~: analz (knows Spy evs)"; 
2032  208 
by (etac yahalom.induct 1); 
6335  209 
by analz_knows_Spy_tac; 
2013  210 
by (ALLGOALS 
211 
(asm_simp_tac 

5535  212 
(simpset() addsimps split_ifs @ pushes @ 
213 
[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

214 
(*Oops*) 
4091  215 
by (blast_tac (claset() addDs [unique_session_keys]) 3); 
2013  216 
(*YM3*) 
4091  217 
by (blast_tac (claset() delrules [impCE] 
6335  218 
addSEs knows_Spy_partsEs 
4238
679a233fb206
Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
paulson
parents:
4091
diff
changeset

219 
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

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

221 
by (spy_analz_tac 1); 
2110  222 
val lemma = result() RS mp RS mp RSN(2,rev_notE); 
2013  223 

224 

3432  225 
(*Final version*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

226 
Goal "[ Says Server A \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

227 
\ {Crypt (shrK A) {Agent B, Key K, na, nb}, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

228 
\ Crypt (shrK B) {Agent A, Key K}} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

229 
\ : set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

230 
\ Notes Spy {na, nb, Key K} ~: set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

231 
\ A ~: bad; B ~: bad; evs : yahalom ] \ 
6335  232 
\ ==> Key K ~: analz (knows Spy evs)"; 
4091  233 
by (blast_tac (claset() addSEs [lemma]) 1); 
2032  234 
qed "Spy_not_see_encrypted_key"; 
2001  235 

236 

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

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

238 

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

239 
(*If the encrypted message appears then it originated with the Server*) 
6335  240 
Goal "[ Crypt (shrK A) {Agent B, Key K, na, nb} : parts (knows Spy evs); \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

241 
\ A ~: bad; evs : yahalom ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

242 
\ ==> Says Server A \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

243 
\ {Crypt (shrK A) {Agent B, Key K, na, nb}, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

244 
\ Crypt (shrK B) {Agent A, Key K}} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

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

247 
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

248 
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

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

250 

4598
649bf14debe7
Added some more explicit guarantees of key secrecy for agents
paulson
parents:
4537
diff
changeset

251 
(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*) 
6335  252 
Goal "[ Crypt (shrK A) {Agent B, Key K, na, nb} : parts (knows Spy evs); \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

253 
\ Notes Spy {na, nb, Key K} ~: set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

254 
\ A ~: bad; B ~: bad; evs : yahalom ] \ 
6335  255 
\ ==> Key K ~: analz (knows Spy evs)"; 
4598
649bf14debe7
Added some more explicit guarantees of key secrecy for agents
paulson
parents:
4537
diff
changeset

256 
by (blast_tac (claset() addSDs [A_trusts_YM3, Spy_not_see_encrypted_key]) 1); 
649bf14debe7
Added some more explicit guarantees of key secrecy for agents
paulson
parents:
4537
diff
changeset

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

258 

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

259 
(** Security Guarantees for B upon receiving YM4 **) 
2013  260 

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

6335  263 
Goal "[ Crypt (shrK B) {Agent A, Key K} : parts (knows Spy evs); \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

264 
\ B ~: bad; evs : yahalom ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

265 
\ ==> EX NA NB. Says Server A \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

266 
\ {Crypt (shrK A) {Agent B, Key K, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

267 
\ Nonce NA, Nonce NB}, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

268 
\ Crypt (shrK B) {Agent A, Key K}} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

269 
\ : set evs"; 
2032  270 
by (etac rev_mp 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

274 
by (Blast_tac 1); 
2110  275 
qed "B_trusts_YM4_shrK"; 
276 

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

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

278 
the key quoting nonce NB. This part says nothing about agent names. 
6335  279 
Secrecy of NB is crucial. Note that Nonce NB ~: analz(knows Spy evs) must 
5065  280 
be the FIRST antecedent of the induction formula.*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

281 
Goal "evs : yahalom \ 
6335  282 
\ ==> Nonce NB ~: analz (knows Spy evs) > \ 
283 
\ Crypt K (Nonce NB) : parts (knows Spy evs) > \ 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

284 
\ (EX A B NA. Says Server A \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

285 
\ {Crypt (shrK A) {Agent B, Key K, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

286 
\ Nonce NA, Nonce NB}, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

287 
\ Crypt (shrK B) {Agent A, Key K}} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

289 
by (parts_induct_tac 1); 
3708  290 
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

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

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

293 
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

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

295 
(*A is uncompromised because NB is secure*) 
6335  296 
by (g_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

297 
(*A's certificate guarantees the existence of the Server message*) 
6335  298 
by (blast_tac (claset() addDs [Says_imp_knows_Spy RS parts.Inj RS parts.Fst RS 
4238
679a233fb206
Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
paulson
parents:
4091
diff
changeset

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

300 
bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp)); 
2133  301 

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

302 

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

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

304 

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

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

306 

5076  307 
Goalw [KeyWithNonce_def] 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

308 
"Says Server A \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

309 
\ {Crypt (shrK A) {Agent B, Key K, na, Nonce NB}, X} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

310 
\ : 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

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

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

313 

5076  314 
Goalw [KeyWithNonce_def] 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

315 
"KeyWithNonce K NB (Says S A X # evs) = \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

316 
\ (Server = S & \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

317 
\ (EX B n X'. X = {Crypt (shrK A) {Agent B, Key K, n, Nonce NB}, X'}) \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

318 
\  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

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

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

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

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

323 

5076  324 
Goalw [KeyWithNonce_def] 
4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

325 
"KeyWithNonce K NB (Notes A X # evs) = KeyWithNonce K NB evs"; 
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

326 
by (Simp_tac 1); 
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

327 
qed "KeyWithNonce_Notes"; 
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

328 
Addsimps [KeyWithNonce_Notes]; 
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

329 

6335  330 
Goalw [KeyWithNonce_def] 
331 
"KeyWithNonce K NB (Gets A X # evs) = KeyWithNonce K NB evs"; 

332 
by (Simp_tac 1); 

333 
qed "KeyWithNonce_Gets"; 

334 
Addsimps [KeyWithNonce_Gets]; 

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). *) 
5076  338 
Goalw [KeyWithNonce_def] 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

339 
"Key K ~: used evs ==> ~ KeyWithNonce K NB evs"; 
6335  340 
by (blast_tac (claset() addSEs knows_Spy_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.*) 
5076  345 
Goalw [KeyWithNonce_def] 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

346 
"[ Says Server A \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

347 
\ {Crypt (shrK A) {Agent B, Key K, na, Nonce NB'}, X} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

348 
\ : set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

349 
\ NB ~= NB'; evs : yahalom ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
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.*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

362 
Goal "P > (X : analz (G Un H)) > (X : analz H) ==> \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

367 
Goal "evs : yahalom ==> \ 
5492  368 
\ (ALL KK. KK <=  (range shrK) > \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

369 
\ (ALL K: KK. ~ KeyWithNonce K NB evs) > \ 
6335  370 
\ (Nonce NB : analz (Key``KK Un (knows Spy evs))) = \ 
371 
\ (Nonce NB : analz (knows Spy evs)))"; 

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

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

374 
by (REPEAT_FIRST (resolve_tac [impI RS allI])); 
3961  375 
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

376 
(*For Oops, simplification proves NBa~=NB. By Says_Server_KeyWithNonce, 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

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

380 
(asm_simp_tac 
3961  381 
(analz_image_freshK_ss 
4831  382 
addsimps split_ifs 
3961  383 
addsimps [all_conj_distrib, analz_image_freshK, 
6335  384 
KeyWithNonce_Says, KeyWithNonce_Notes, KeyWithNonce_Gets, 
5073  385 
fresh_not_KeyWithNonce, Says_Server_not_range, 
3961  386 
imp_disj_not1, (*Moves NBa~=NB to the front*) 
387 
Says_Server_KeyWithNonce]))); 

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

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

389 
by (spy_analz_tac 1); 
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4238
diff
changeset

390 
(*YM4*) (** LEVEL 6 **) 
6335  391 
by (g_not_bad_tac "A" 1); 
392 
by (dtac (Gets_imp_knows_Spy 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

393 
THEN REPEAT (assume_tac 1)); 
4091  394 
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

395 
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

396 

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

397 

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

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

399 
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

400 
for the induction to carry through.*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

401 
Goal "[ Says Server A \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

402 
\ {Crypt (shrK A) {Agent B, Key KAB, na, Nonce NB'}, X} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

403 
\ : set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

404 
\ NB ~= NB'; KAB ~: range shrK; evs : yahalom ] \ 
6335  405 
\ ==> (Nonce NB : analz (insert (Key KAB) (knows Spy evs))) = \ 
406 
\ (Nonce NB : analz (knows Spy evs))"; 

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

407 
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

408 
[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

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

410 

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

411 

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

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

413 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

414 
Goal "evs : yahalom ==> \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

415 
\EX NA' A' B'. ALL NA A B. \ 
6335  416 
\ Crypt (shrK B) {Agent A, Nonce NA, nb} : parts(knows Spy evs) \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

417 
\ > 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

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

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

420 
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

421 
THEN Fake_parts_insert_tac 1); 
4091  422 
by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1); 
2133  423 
(*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

424 
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

425 
by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1)); 
6335  426 
by (blast_tac (claset() addSEs knows_Spy_partsEs) 1); 
2133  427 
val lemma = result(); 
428 

6335  429 
Goal "[ Crypt (shrK B) {Agent A, Nonce NA, nb} : parts (knows Spy evs); \ 
430 
\ Crypt (shrK B') {Agent A', Nonce NA', nb} : parts (knows Spy evs); \ 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

431 
\ evs : yahalom; B ~: bad; B' ~: bad ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

433 
by (prove_unique_tac lemma 1); 
2133  434 
qed "unique_NB"; 
435 

436 

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

437 
(*Variant useful for proving secrecy of NB: the Says... form allows 
3683  438 
not_bad_tac to remove the assumption B' ~: bad.*) 
6335  439 
Goal "[ Says C S {X, Crypt (shrK B) {Agent A, Nonce NA, nb}} \ 
440 
\ : set evs; B ~: bad; \ 

441 
\ Gets S' {X', Crypt (shrK B') {Agent A', Nonce NA', nb}} \ 

442 
\ : set evs; \ 

443 
\ nb ~: analz (knows Spy evs); evs : yahalom ] \ 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

444 
\ ==> NA' = NA & A' = A & B' = B"; 
6335  445 
by (g_not_bad_tac "B'" 1); 
446 
by (blast_tac (claset() addSDs [Says_imp_knows_Spy RS parts.Inj] 

4238
679a233fb206
Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
paulson
parents:
4091
diff
changeset

447 
addSEs [MPair_parts] 
679a233fb206
Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
paulson
parents:
4091
diff
changeset

448 
addDs [unique_NB]) 1); 
2133  449 
qed "Says_unique_NB"; 
450 

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

451 

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

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

453 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

454 
Goal "evs : yahalom \ 
6335  455 
\ ==> Nonce NB ~: analz (knows Spy evs) > \ 
456 
\ Crypt (shrK B') {Agent A', Nonce NB, nb'} : parts(knows Spy evs) > \ 

457 
\ Crypt (shrK B) {Agent A, na, Nonce NB} ~: parts(knows Spy evs)"; 

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

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

459 
by (Fake_parts_insert_tac 1); 
6335  460 
by (blast_tac (claset() addDs [Gets_imp_knows_Spy RS analz.Inj] 
4238
679a233fb206
Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
paulson
parents:
4091
diff
changeset

461 
addSIs [parts_insertI] 
679a233fb206
Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
paulson
parents:
4091
diff
changeset

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

463 
bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE)); 
2133  464 

5065  465 
(*more readable version cited in Yahalom paper*) 
466 
standard (result() RS mp RSN (2,rev_mp)); 

467 

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

468 
(*The Server sends YM3 only in response to YM2.*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

469 
Goal "[ Says Server A \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

470 
\ {Crypt (shrK A) {Agent B, k, na, nb}, X} : set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

471 
\ evs : yahalom ] \ 
6335  472 
\ ==> Gets Server { Agent B, Crypt (shrK B) {Agent A, na, nb} } \ 
473 
\ : set evs"; 

2133  474 
by (etac rev_mp 1); 
475 
by (etac yahalom.induct 1); 

5932  476 
by Auto_tac; 
2133  477 
qed "Says_Server_imp_YM2"; 
478 

479 

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

480 
(*A vital theorem for B, that nonce NB remains secure from the Spy.*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

481 
Goal "[ A ~: bad; B ~: bad; evs : yahalom ] \ 
2133  482 
\ ==> Says B Server \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

483 
\ {Agent B, Crypt (shrK B) {Agent A, Nonce NA, Nonce NB}} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

484 
\ : set evs > \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

485 
\ (ALL k. Notes Spy {Nonce NA, Nonce NB, k} ~: set evs) > \ 
6335  486 
\ Nonce NB ~: analz (knows Spy evs)"; 
2133  487 
by (etac yahalom.induct 1); 
6335  488 
by analz_knows_Spy_tac; 
2133  489 
by (ALLGOALS 
490 
(asm_simp_tac 

5535  491 
(simpset() addsimps split_ifs @ pushes @ 
492 
[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

493 
(*Prove YM3 by showing that no NB can also be an NA*) 
6335  494 
by (blast_tac (claset() addDs [Says_imp_knows_Spy RS parts.Inj] 
9166  495 
addSEs [no_nonce_YM1_YM2, MPair_parts] 
496 
addDs [Gets_imp_Says, Says_unique_NB]) 4); 

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

497 
(*YM2: similar freshness reasoning*) 
4091  498 
by (blast_tac (claset() addSEs partsEs 
6335  499 
addDs [Gets_imp_Says, 
500 
Says_imp_knows_Spy RS analz.Inj, 

4238
679a233fb206
Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
paulson
parents:
4091
diff
changeset

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

502 
(*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*) 
4091  503 
by (blast_tac (claset() addSIs [parts_insertI] 
6335  504 
addSEs knows_Spy_partsEs) 2); 
2377  505 
(*Fake*) 
506 
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

507 
(** LEVEL 7: YM4 and Oops remain **) 
5932  508 
by (ALLGOALS (Clarify_tac THEN' 
509 
full_simp_tac (simpset() addsimps [all_conj_distrib]))); 

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

510 
(*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) 
6335  511 
by (g_not_bad_tac "Aa" 1); 
512 
by (dtac (Gets_imp_knows_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1 

513 
THEN assume_tac 1); 

7499  514 
by (ftac Says_Server_imp_YM2 3); 
5932  515 
by (REPEAT_FIRST (eresolve_tac [asm_rl, exE])); 
516 
(* use Says_unique_NB to identify message components: Aa=A, Ba=B*) 

6335  517 
by (blast_tac (claset() addDs [Says_unique_NB, 
518 
Spy_not_see_encrypted_key]) 1); 

5073  519 
(** LEVEL 13 **) 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

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

521 
covered by the quantified Oops assumption.*) 
7499  522 
by (ftac Says_Server_imp_YM2 1 THEN assume_tac 1); 
2133  523 
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

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

526 
(*case NB ~= NBa*) 
4091  527 
by (asm_simp_tac (simpset() addsimps [single_Nonce_secrecy]) 1); 
4471  528 
by (Clarify_tac 1); 
9166  529 
by (blast_tac (claset() addSEs [MPair_parts, no_nonce_YM1_YM2] 
530 
(*to prove NB~=NAa*) 

531 
addDs [Says_imp_knows_Spy 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

532 
bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp)); 
2133  533 

2001  534 

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

535 
(*B's session key guarantee from YM4. The two certificates contribute to a 
4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

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

537 
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

538 
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

539 
old key, B has no means of telling.*) 
6335  540 
Goal "[ Gets B {Crypt (shrK B) {Agent A, Key K}, \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

541 
\ Crypt K (Nonce NB)} : set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

542 
\ Says B Server \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

543 
\ {Agent B, Crypt (shrK B) {Agent A, Nonce NA, Nonce NB}} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

544 
\ : set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

545 
\ ALL k. Notes Spy {Nonce NA, Nonce NB, k} ~: set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

546 
\ A ~: bad; B ~: bad; evs : yahalom ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

547 
\ ==> Says Server A \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

548 
\ {Crypt (shrK A) {Agent B, Key K, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

549 
\ Nonce NA, Nonce NB}, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

550 
\ Crypt (shrK B) {Agent A, Key K}} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

551 
\ : set evs"; 
7499  552 
by (ftac Spy_not_see_NB 1 THEN REPEAT (assume_tac 1)); 
6335  553 
by (etac (Gets_imp_knows_Spy RS parts.Inj RS MPair_parts) 1 THEN 
554 
assume_tac 1 THEN dtac B_trusts_YM4_shrK 1); 

2170  555 
by (dtac B_trusts_YM4_newK 3); 
2110  556 
by (REPEAT_FIRST (eresolve_tac [asm_rl, exE])); 
7499  557 
by (ftac Says_Server_imp_YM2 1 THEN assume_tac 1); 
2170  558 
by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1)); 
4091  559 
by (blast_tac (claset() addDs [Says_unique_NB]) 1); 
2322  560 
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

561 

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

562 

4598
649bf14debe7
Added some more explicit guarantees of key secrecy for agents
paulson
parents:
4537
diff
changeset

563 
(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*) 
6335  564 
Goal "[ Gets B {Crypt (shrK B) {Agent A, Key K}, \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

565 
\ Crypt K (Nonce NB)} : set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

566 
\ Says B Server \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

567 
\ {Agent B, Crypt (shrK B) {Agent A, Nonce NA, Nonce NB}} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

568 
\ : set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

569 
\ ALL k. Notes Spy {Nonce NA, Nonce NB, k} ~: set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

570 
\ A ~: bad; B ~: bad; evs : yahalom ] \ 
6335  571 
\ ==> Key K ~: analz (knows Spy evs)"; 
4598
649bf14debe7
Added some more explicit guarantees of key secrecy for agents
paulson
parents:
4537
diff
changeset

572 
by (blast_tac (claset() addSDs [B_trusts_YM4, Spy_not_see_encrypted_key]) 1); 
649bf14debe7
Added some more explicit guarantees of key secrecy for agents
paulson
parents:
4537
diff
changeset

573 
qed "B_gets_good_key"; 
649bf14debe7
Added some more explicit guarantees of key secrecy for agents
paulson
parents:
4537
diff
changeset

574 

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

575 

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

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

577 

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

578 
(*The encryption in message YM2 tells us it cannot be faked.*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

579 
Goal "evs : yahalom \ 
6335  580 
\ ==> Crypt (shrK B) {Agent A, Nonce NA, nb} : parts (knows Spy evs) > \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

581 
\ B ~: bad > \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

582 
\ Says B Server {Agent B, Crypt (shrK B) {Agent A, Nonce NA, nb}} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

584 
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

585 
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

586 
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

587 

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

588 
(*If the server sends YM3 then B sent YM2*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

590 
\ ==> Says Server A {Crypt (shrK A) {Agent B, Key K, Nonce NA, nb}, X} \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

591 
\ : set evs > \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

592 
\ B ~: bad > \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

593 
\ Says B Server {Agent B, Crypt (shrK B) {Agent A, Nonce NA, nb}} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

595 
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

596 
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

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

598 
by (Blast_tac 2); 
4509
828148415197
Making proofs faster, especially using keysFor_parts_insert
paulson
parents:
4477
diff
changeset

599 
(*YM3 [blast_tac is 50% slower] *) 
6335  600 
by (best_tac (claset() addSDs [B_Said_YM2, Says_imp_knows_Spy RS parts.Inj] 
4238
679a233fb206
Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
paulson
parents:
4091
diff
changeset

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

602 
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

603 

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

604 
(*If A receives YM3 then B has used nonce NA (and therefore is alive)*) 
6335  605 
Goal "[ Gets A {Crypt (shrK A) {Agent B, Key K, Nonce NA, nb}, X} \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

606 
\ : set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

607 
\ A ~: bad; B ~: bad; evs : yahalom ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

608 
\==> Says B Server {Agent B, Crypt (shrK B) {Agent A, Nonce NA, nb}} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

609 
\ : set evs"; 
4091  610 
by (blast_tac (claset() addSDs [A_trusts_YM3, lemma] 
6335  611 
addEs knows_Spy_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.*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

620 
Goal "evs : yahalom \ 
6335  621 
\ ==> Key K ~: analz (knows Spy evs) > \ 
622 
\ Crypt K (Nonce NB) : parts (knows Spy evs) > \ 

623 
\ Crypt (shrK B) {Agent A, Key K} : parts (knows Spy evs) > \ 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

624 
\ B ~: bad > \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

626 
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

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

628 
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

629 
(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*) 
4238
679a233fb206
Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
paulson
parents:
4091
diff
changeset

630 
by (fast_tac (claset() addSDs [Crypt_imp_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

631 
(*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*) 
4091  632 
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

633 
(*yes: apply unicity of session keys*) 
6335  634 
by (g_not_bad_tac "Aa" 1); 
4091  635 
by (blast_tac (claset() addSEs [MPair_parts] 
4238
679a233fb206
Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
paulson
parents:
4091
diff
changeset

636 
addSDs [A_trusts_YM3, B_trusts_YM4_shrK] 
6335  637 
addDs [Says_imp_knows_Spy RS parts.Inj, 
4238
679a233fb206
Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
paulson
parents:
4091
diff
changeset

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

640 

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

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

642 
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

643 
Other premises guarantee secrecy of K.*) 
6335  644 
Goal "[ Gets B {Crypt (shrK B) {Agent A, Key K}, \ 
645 
\ Crypt K (Nonce NB)} : set evs; \ 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

646 
\ Says B Server \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

647 
\ {Agent B, Crypt (shrK B) {Agent A, Nonce NA, Nonce NB}} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

648 
\ : set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

649 
\ (ALL NA k. Notes Spy {Nonce NA, Nonce NB, k} ~: set evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

650 
\ A ~: bad; B ~: bad; evs : yahalom ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

651 
\ ==> EX X. Says A B {X, Crypt K (Nonce NB)} : set evs"; 
7499  652 
by (ftac B_trusts_YM4 1); 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

653 
by (REPEAT_FIRST (eresolve_tac [asm_rl, spec])); 
6335  654 
by (etac (Gets_imp_knows_Spy RS parts.Inj RS MPair_parts) 1 THEN assume_tac 1); 
655 
by (rtac A_Said_YM3_lemma 1); 

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

656 
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

657 
by (REPEAT_FIRST assume_tac); 
4091  658 
by (blast_tac (claset() addSEs [MPair_parts] 
6335  659 
addDs [Says_imp_knows_Spy 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

660 
qed_spec_mp "YM4_imp_A_Said_YM3"; 