author  paulson 
Thu, 23 Jan 1997 10:34:18 +0100  
changeset 2536  1e04eb7f7eb1 
parent 2516  4d68fbe6378b 
child 2637  e9b203f854ae 
permissions  rwrr 
2318  1 
(* Title: HOL/Auth/NS_Public_Bad 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1996 University of Cambridge 

5 

6 
Inductive relation "ns_public" for the NeedhamSchroeder PublicKey protocol. 

7 
Flawed version, vulnerable to Lowe's attack. 

8 

9 
From page 260 of 

10 
Burrows, Abadi and Needham. A Logic of Authentication. 

11 
Proc. Royal Soc. 426 (1989) 

12 
*) 

13 

14 
open NS_Public_Bad; 

15 

16 
proof_timing:=true; 

17 
HOL_quantifiers := false; 

18 

19 
AddIffs [Spy_in_lost]; 

20 

21 
(*Replacing the variable by a constant improves search speed by 50%!*) 

22 
val Says_imp_sees_Spy' = 

23 
read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy; 

24 

25 

26 
(*A "possibility property": there are traces that reach the end*) 

27 
goal thy 

2480  28 
"!!A B. A ~= B ==> EX NB. EX evs: ns_public. \ 
29 
\ Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs"; 

2318  30 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
31 
by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2); 

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

32 
by possibility_tac; 
2318  33 
result(); 
34 

35 

36 
(**** Inductive proofs about ns_public ****) 

37 

38 
(*Nobody sends themselves messages*) 

39 
goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set_of_list evs"; 

40 
by (etac ns_public.induct 1); 

41 
by (Auto_tac()); 

42 
qed_spec_mp "not_Says_to_self"; 

43 
Addsimps [not_Says_to_self]; 

44 
AddSEs [not_Says_to_self RSN (2, rev_notE)]; 

45 

46 

47 
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) 

48 
fun parts_induct_tac i = SELECT_GOAL 

49 
(DETERM (etac ns_public.induct 1 THEN 

50 
(*Fake message*) 

51 
TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, 

52 
impOfSubs Fake_parts_insert] 

53 
addss (!simpset)) 2)) THEN 

54 
(*Base case*) 

55 
fast_tac (!claset addss (!simpset)) 1 THEN 

56 
ALLGOALS Asm_simp_tac) i; 

57 

58 
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY 

59 
sends messages containing X! **) 

60 

61 
(*Spy never sees another agent's private key! (unless it's lost at start)*) 

62 
goal thy 

63 
"!!evs. evs : ns_public \ 

64 
\ ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)"; 

65 
by (parts_induct_tac 1); 

66 
by (Auto_tac()); 

67 
qed "Spy_see_priK"; 

68 
Addsimps [Spy_see_priK]; 

69 

70 
goal thy 

71 
"!!evs. evs : ns_public \ 

72 
\ ==> (Key (priK A) : analz (sees lost Spy evs)) = (A : lost)"; 

73 
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); 

74 
qed "Spy_analz_priK"; 

75 
Addsimps [Spy_analz_priK]; 

76 

77 
goal thy "!!A. [ Key (priK A) : parts (sees lost Spy evs); \ 

78 
\ evs : ns_public ] ==> A:lost"; 

79 
by (fast_tac (!claset addDs [Spy_see_priK]) 1); 

80 
qed "Spy_see_priK_D"; 

81 

82 
bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D); 

83 
AddSDs [Spy_see_priK_D, Spy_analz_priK_D]; 

84 

85 

2418
6b6a92d05fb2
New tactics: prove_unique_tac and analz_induct_tac
paulson
parents:
2374
diff
changeset

86 
fun analz_induct_tac i = 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset

87 
etac ns_public.induct i THEN 
2418
6b6a92d05fb2
New tactics: prove_unique_tac and analz_induct_tac
paulson
parents:
2374
diff
changeset

88 
ALLGOALS (asm_simp_tac 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset

89 
(!simpset addsimps [not_parts_not_analz] 
2480  90 
setloop split_tac [expand_if])); 
2418
6b6a92d05fb2
New tactics: prove_unique_tac and analz_induct_tac
paulson
parents:
2374
diff
changeset

91 

2318  92 

93 
(**** Authenticity properties obtained from NS2 ****) 

94 

95 
(*It is impossible to reuse a nonce in both NS1 and NS2, provided the nonce 

96 
is secret. (Honest users generate fresh nonces.)*) 

97 
goal thy 

2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

98 
"!!evs. [ Nonce NA ~: analz (sees lost Spy evs); \ 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

99 
\ Crypt (pubK B) {Nonce NA, Agent A} : parts (sees lost Spy evs); \ 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

100 
\ evs : ns_public ] \ 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

101 
\ ==> Crypt (pubK C) {NA', Nonce NA} ~: parts (sees lost Spy evs)"; 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

102 
by (etac rev_mp 1); 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

103 
by (etac rev_mp 1); 
2418
6b6a92d05fb2
New tactics: prove_unique_tac and analz_induct_tac
paulson
parents:
2374
diff
changeset

104 
by (analz_induct_tac 1); 
2318  105 
(*NS3*) 
2497  106 
by (fast_tac (!claset addSEs partsEs) 4); 
2318  107 
(*NS2*) 
2497  108 
by (fast_tac (!claset addSEs partsEs) 3); 
2318  109 
(*Fake*) 
2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

110 
by (deepen_tac (!claset addSIs [analz_insertI] 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

111 
addDs [impOfSubs analz_subset_parts, 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

112 
impOfSubs Fake_parts_insert] 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

113 
addss (!simpset)) 0 2); 
2318  114 
(*Base*) 
2374  115 
by (fast_tac (!claset addss (!simpset)) 1); 
2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

116 
qed "no_nonce_NS1_NS2"; 
2318  117 

118 

2480  119 
(*Unicity for NS1: nonce NA identifies agents A and B*) 
2318  120 
goal thy 
2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

121 
"!!evs. [ Nonce NA ~: analz (sees lost Spy evs); evs : ns_public ] \ 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

122 
\ ==> EX A' B'. ALL A B. \ 
2318  123 
\ Crypt (pubK B) {Nonce NA, Agent A} : parts (sees lost Spy evs) > \ 
2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

124 
\ A=A' & B=B'"; 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

125 
by (etac rev_mp 1); 
2418
6b6a92d05fb2
New tactics: prove_unique_tac and analz_induct_tac
paulson
parents:
2374
diff
changeset

126 
by (analz_induct_tac 1); 
2318  127 
(*NS1*) 
2497  128 
by (simp_tac (!simpset addsimps [all_conj_distrib]) 3); 
2318  129 
by (expand_case_tac "NA = ?y" 3 THEN 
2497  130 
REPEAT (fast_tac (!claset addSEs partsEs) 3)); 
2318  131 
(*Base*) 
132 
by (fast_tac (!claset addss (!simpset)) 1); 

133 
(*Fake*) 

2497  134 
by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1); 
2374  135 
by (step_tac (!claset addSIs [analz_insertI]) 1); 
2318  136 
by (ex_strip_tac 1); 
137 
by (best_tac (!claset delrules [conjI] 

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

138 
addSDs [impOfSubs Fake_parts_insert] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset

139 
addDs [impOfSubs analz_subset_parts] 
2318  140 
addss (!simpset)) 1); 
141 
val lemma = result(); 

142 

143 
goal thy 

144 
"!!evs. [ Crypt(pubK B) {Nonce NA, Agent A} : parts(sees lost Spy evs); \ 

145 
\ Crypt(pubK B') {Nonce NA, Agent A'} : parts(sees lost Spy evs); \ 

146 
\ Nonce NA ~: analz (sees lost Spy evs); \ 

147 
\ evs : ns_public ] \ 

148 
\ ==> A=A' & B=B'"; 

2418
6b6a92d05fb2
New tactics: prove_unique_tac and analz_induct_tac
paulson
parents:
2374
diff
changeset

149 
by (prove_unique_tac lemma 1); 
2318  150 
qed "unique_NA"; 
151 

152 

153 
(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*) 

154 
goal thy 

2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

155 
"!!evs. [ Says A B (Crypt(pubK B) {Nonce NA, Agent A}) : set_of_list evs; \ 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

156 
\ A ~: lost; B ~: lost; evs : ns_public ] \ 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

157 
\ ==> Nonce NA ~: analz (sees lost Spy evs)"; 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

158 
by (etac rev_mp 1); 
2418
6b6a92d05fb2
New tactics: prove_unique_tac and analz_induct_tac
paulson
parents:
2374
diff
changeset

159 
by (analz_induct_tac 1); 
2318  160 
(*NS3*) 
161 
by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] 

162 
addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4); 

2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

163 
(*NS2*) 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

164 
by (deepen_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

165 
addSEs [MPair_parts] 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

166 
addDs [parts.Body, unique_NA]) 0 3); 
2318  167 
(*NS1*) 
2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

168 
by (fast_tac (!claset addSEs sees_Spy_partsEs 
2497  169 
addIs [impOfSubs analz_subset_parts]) 2); 
2318  170 
(*Fake*) 
2497  171 
by (spy_analz_tac 1); 
2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

172 
qed "Spy_not_see_NA"; 
2318  173 

174 

175 
(*Authentication for A: if she receives message 2 and has used NA 

176 
to start a run, then B has sent message 2.*) 

177 
goal thy 

2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

178 
"!!evs. [ Says A B (Crypt (pubK B) {Nonce NA, Agent A}) : set_of_list evs;\ 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

179 
\ Says B' A (Crypt(pubK A) {Nonce NA, Nonce NB}): set_of_list evs;\ 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

180 
\ A ~: lost; B ~: lost; evs : ns_public ] \ 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

181 
\ ==> Says B A (Crypt(pubK A) {Nonce NA, Nonce NB}): set_of_list evs"; 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

182 
by (etac rev_mp 1); 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

183 
(*prepare induction over Crypt (pubK A) {NA,NB} : parts H*) 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

184 
by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1); 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

185 
by (etac ns_public.induct 1); 
2318  186 
by (ALLGOALS Asm_simp_tac); 
187 
(*NS1*) 

2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

188 
by (fast_tac (!claset addSEs sees_Spy_partsEs) 2); 
2318  189 
(*Fake*) 
190 
by (REPEAT_FIRST (resolve_tac [impI, conjI])); 

191 
by (fast_tac (!claset addss (!simpset)) 1); 

192 
by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1)); 

2324  193 
by (best_tac (!claset addSIs [disjI2] 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset

194 
addSDs [impOfSubs Fake_parts_insert] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset

195 
addDs [impOfSubs analz_subset_parts] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset

196 
addss (!simpset)) 1); 
2318  197 
(*NS2*) 
198 
by (Step_tac 1); 

199 
by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1)); 

2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

200 
by (deepen_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

201 
addDs [unique_NA]) 1 1); 
2318  202 
qed "A_trusts_NS2"; 
203 

204 
(*If the encrypted message appears then it originated with Alice in NS1*) 

205 
goal thy 

2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

206 
"!!evs. [ Crypt (pubK B) {Nonce NA, Agent A} : parts (sees lost Spy evs); \ 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

207 
\ Nonce NA ~: analz (sees lost Spy evs); \ 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

208 
\ evs : ns_public ] \ 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

209 
\ ==> Says A B (Crypt (pubK B) {Nonce NA, Agent A}) : set_of_list evs"; 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

210 
by (etac rev_mp 1); 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

211 
by (etac rev_mp 1); 
2418
6b6a92d05fb2
New tactics: prove_unique_tac and analz_induct_tac
paulson
parents:
2374
diff
changeset

212 
by (analz_induct_tac 1); 
2318  213 
(*Fake*) 
214 
by (best_tac (!claset addSIs [disjI2] 

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

215 
addSDs [impOfSubs Fake_parts_insert] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset

216 
addIs [analz_insertI] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset

217 
addDs [impOfSubs analz_subset_parts] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset

218 
addss (!simpset)) 2); 
2318  219 
(*Base*) 
220 
by (fast_tac (!claset addss (!simpset)) 1); 

221 
qed_spec_mp "B_trusts_NS1"; 

222 

223 

224 

225 
(**** Authenticity properties obtained from NS2 ****) 

226 

2480  227 
(*Unicity for NS2: nonce NB identifies agent A and nonce NA 
2318  228 
[proof closely follows that for unique_NA] *) 
229 
goal thy 

2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

230 
"!!evs. [ Nonce NB ~: analz (sees lost Spy evs); evs : ns_public ] \ 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

231 
\ ==> EX A' NA'. ALL A NA. \ 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

232 
\ Crypt (pubK A) {Nonce NA, Nonce NB} \ 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

233 
\ : parts (sees lost Spy evs) > A=A' & NA=NA'"; 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

234 
by (etac rev_mp 1); 
2418
6b6a92d05fb2
New tactics: prove_unique_tac and analz_induct_tac
paulson
parents:
2374
diff
changeset

235 
by (analz_induct_tac 1); 
2318  236 
(*NS2*) 
2497  237 
by (simp_tac (!simpset addsimps [all_conj_distrib]) 3); 
2318  238 
by (expand_case_tac "NB = ?y" 3 THEN 
2497  239 
REPEAT (fast_tac (!claset addSEs partsEs) 3)); 
2318  240 
(*Base*) 
241 
by (fast_tac (!claset addss (!simpset)) 1); 

242 
(*Fake*) 

2497  243 
by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1); 
2374  244 
by (step_tac (!claset addSIs [analz_insertI]) 1); 
2318  245 
by (ex_strip_tac 1); 
246 
by (best_tac (!claset delrules [conjI] 

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

247 
addSDs [impOfSubs Fake_parts_insert] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset

248 
addDs [impOfSubs analz_subset_parts] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset

249 
addss (!simpset)) 1); 
2318  250 
val lemma = result(); 
251 

252 
goal thy 

253 
"!!evs. [ Crypt(pubK A) {Nonce NA, Nonce NB} : parts(sees lost Spy evs); \ 

254 
\ Crypt(pubK A'){Nonce NA', Nonce NB} : parts(sees lost Spy evs); \ 

255 
\ Nonce NB ~: analz (sees lost Spy evs); \ 

256 
\ evs : ns_public ] \ 

257 
\ ==> A=A' & NA=NA'"; 

2418
6b6a92d05fb2
New tactics: prove_unique_tac and analz_induct_tac
paulson
parents:
2374
diff
changeset

258 
by (prove_unique_tac lemma 1); 
2318  259 
qed "unique_NB"; 
260 

261 

262 
(*NB remains secret PROVIDED Alice never responds with round 3*) 

263 
goal thy 

2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

264 
"!!evs.[ Says B A (Crypt (pubK A) {Nonce NA, Nonce NB}) : set_of_list evs;\ 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

265 
\ (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set_of_list evs); \ 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

266 
\ A ~: lost; B ~: lost; evs : ns_public ] \ 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

267 
\ ==> Nonce NB ~: analz (sees lost Spy evs)"; 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

268 
by (etac rev_mp 1); 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

269 
by (etac rev_mp 1); 
2418
6b6a92d05fb2
New tactics: prove_unique_tac and analz_induct_tac
paulson
parents:
2374
diff
changeset

270 
by (analz_induct_tac 1); 
2318  271 
(*NS1*) 
2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

272 
by (fast_tac (!claset addSEs sees_Spy_partsEs) 2); 
2318  273 
(*Fake*) 
2497  274 
by (spy_analz_tac 1); 
2318  275 
(*NS2 and NS3*) 
2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

276 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

277 
by (step_tac (!claset delrules [allI]) 1); 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

278 
by (Fast_tac 5); 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

279 
by (fast_tac (!claset addSIs [impOfSubs analz_subset_parts]) 1); 
2318  280 
(*NS2*) 
2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

281 
by (fast_tac (!claset addSEs sees_Spy_partsEs) 2); 
2497  282 
by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] 
283 
addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1); 

2318  284 
(*NS3*) 
285 
by (forw_inst_tac [("A'","A")] (Says_imp_sees_Spy' RS parts.Inj RS unique_NB) 1 

286 
THEN REPEAT (eresolve_tac [asm_rl, Says_imp_sees_Spy' RS parts.Inj] 1)); 

287 
by (Fast_tac 1); 

2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

288 
qed "Spy_not_see_NB"; 
2318  289 

290 

291 

292 
(*Authentication for B: if he receives message 3 and has used NB 

2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

293 
in message 2, then A has sent message 3to somebody....*) 
2318  294 
goal thy 
2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

295 
"!!evs. [ Says B A (Crypt (pubK A) {Nonce NA, Nonce NB}) \ 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

296 
\ : set_of_list evs; \ 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

297 
\ Says A' B (Crypt (pubK B) (Nonce NB)): set_of_list evs; \ 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

298 
\ A ~: lost; B ~: lost; evs : ns_public ] \ 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

299 
\ ==> EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set_of_list evs"; 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

300 
by (etac rev_mp 1); 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

301 
(*prepare induction over Crypt (pubK B) NB : parts H*) 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

302 
by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1); 
2418
6b6a92d05fb2
New tactics: prove_unique_tac and analz_induct_tac
paulson
parents:
2374
diff
changeset

303 
by (analz_induct_tac 1); 
2318  304 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); 
305 
(*NS1*) 

2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

306 
by (fast_tac (!claset addSEs sees_Spy_partsEs) 2); 
2318  307 
(*Fake*) 
308 
by (REPEAT_FIRST (resolve_tac [impI, conjI])); 

309 
by (fast_tac (!claset addss (!simpset)) 1); 

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

310 
by (rtac (ccontr RS disjI2) 1); 
2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

311 
by (forward_tac [Spy_not_see_NB] 1 THEN (REPEAT_FIRST assume_tac) 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

312 
THEN Fast_tac 1); 
2318  313 
by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert] 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset

314 
addDs [impOfSubs analz_subset_parts] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset

315 
addss (!simpset)) 1); 
2318  316 
(*NS3*) 
317 
by (Step_tac 1); 

2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

318 
by (forward_tac [Spy_not_see_NB] 1 THEN (REPEAT_FIRST assume_tac) 
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

319 
THEN Fast_tac 1); 
2318  320 
by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset

321 
addDs [unique_NB]) 1); 
2318  322 
qed "B_trusts_NS3"; 
323 

324 

325 
(*Can we strengthen the secrecy theorem? NO*) 

326 
goal thy 

327 
"!!evs. [ A ~: lost; B ~: lost; evs : ns_public ] \ 

328 
\ ==> Says B A (Crypt (pubK A) {Nonce NA, Nonce NB}) : set_of_list evs \ 

329 
\ > Nonce NB ~: analz (sees lost Spy evs)"; 

2418
6b6a92d05fb2
New tactics: prove_unique_tac and analz_induct_tac
paulson
parents:
2374
diff
changeset

330 
by (analz_induct_tac 1); 
2318  331 
(*NS1*) 
332 
by (fast_tac (!claset addSEs partsEs 

2497  333 
addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2); 
2318  334 
(*Fake*) 
2497  335 
by (spy_analz_tac 1); 
2318  336 
(*NS2 and NS3*) 
337 
by (Step_tac 1); 

2497  338 
by (fast_tac (!claset addSIs [impOfSubs analz_subset_parts, usedI]) 1); 
2318  339 
(*NS2*) 
340 
by (fast_tac (!claset addSEs partsEs 

2497  341 
addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2); 
2318  342 
by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] 
343 
addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1); 

344 
(*NS3*) 

345 
by (forw_inst_tac [("A'","A")] (Says_imp_sees_Spy' RS parts.Inj RS unique_NB) 1 

346 
THEN REPEAT (eresolve_tac [asm_rl, Says_imp_sees_Spy' RS parts.Inj] 1)); 

347 
by (Step_tac 1); 

348 

349 
(* 

350 
THIS IS THE ATTACK! 

351 
Level 9 

352 
!!evs. [ A ~: lost; B ~: lost; evs : ns_public ] 

353 
==> Says B A (Crypt (pubK A) {Nonce NA, Nonce NB}) 

354 
: set_of_list evs > 

355 
Nonce NB ~: analz (sees lost Spy evs) 

356 
1. !!evs Aa Ba B' NAa NBa evsa. 

357 
[ A ~: lost; B ~: lost; evsa : ns_public; A ~= Ba; 

358 
Says B' A (Crypt (pubK A) {Nonce NA, Nonce NB}) : set_of_list evsa; 

359 
Says A Ba (Crypt (pubK Ba) {Nonce NA, Agent A}) : set_of_list evsa; 

360 
Ba : lost; 

361 
Says B A (Crypt (pubK A) {Nonce NA, Nonce NB}) : set_of_list evsa; 

362 
Nonce NB ~: analz (sees lost Spy evsa) ] 

363 
==> False 

364 
*) 

365 

366 

367 