author  paulson 
Thu, 25 Sep 1997 12:14:41 +0200  
changeset 3709  c13c2137e9ee 
parent 3703  c5ae2d63dbaa 
child 3919  c036caebfc75 
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 

3683  19 
AddIffs [Spy_in_bad]; 
2318  20 

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

22 
goal thy 

2480  23 
"!!A B. A ~= B ==> EX NB. EX evs: ns_public. \ 
3465  24 
\ Says A B (Crypt (pubK B) (Nonce NB)) : set evs"; 
2318  25 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
26 
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

27 
by possibility_tac; 
2318  28 
result(); 
29 

30 

31 
(**** Inductive proofs about ns_public ****) 

32 

33 
(*Nobody sends themselves messages*) 

3465  34 
goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set evs"; 
2318  35 
by (etac ns_public.induct 1); 
36 
by (Auto_tac()); 

37 
qed_spec_mp "not_Says_to_self"; 

38 
Addsimps [not_Says_to_self]; 

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

40 

41 

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

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

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

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

46 
etac ns_public.induct i 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

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

48 
REPEAT (FIRSTGOAL analz_mono_contra_tac) 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

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

50 
prove_simple_subgoals_tac i; 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

51 

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

52 

3683  53 
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY 
2318  54 
sends messages containing X! **) 
55 

3683  56 
(*Spy never sees another agent's private key! (unless it's bad at start)*) 
2318  57 
goal thy 
3683  58 
"!!A. evs: ns_public ==> (Key (priK A) : parts (spies evs)) = (A : bad)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

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

60 
by (Fake_parts_insert_tac 1); 
2318  61 
qed "Spy_see_priK"; 
62 
Addsimps [Spy_see_priK]; 

63 

64 
goal thy 

3683  65 
"!!A. evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)"; 
2318  66 
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); 
67 
qed "Spy_analz_priK"; 

68 
Addsimps [Spy_analz_priK]; 

69 

3683  70 
goal thy "!!A. [ Key (priK A) : parts (spies evs); \ 
71 
\ evs : ns_public ] ==> A:bad"; 

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

72 
by (blast_tac (!claset addDs [Spy_see_priK]) 1); 
2318  73 
qed "Spy_see_priK_D"; 
74 

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

76 
AddSDs [Spy_see_priK_D, Spy_analz_priK_D]; 

77 

78 

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

79 
(**** Authenticity properties obtained from NS2 ****) 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

80 

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

81 
(*It is impossible to reuse a nonce in both NS1 and NS2, provided the nonce 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

82 
is secret. (Honest users generate fresh nonces.)*) 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

83 
goal thy 
3683  84 
"!!evs. [ Crypt (pubK B) {Nonce NA, Agent A} : parts (spies evs); \ 
85 
\ Nonce NA ~: analz (spies evs); evs : ns_public ] \ 

86 
\ ==> Crypt (pubK C) {NA', Nonce NA} ~: parts (spies evs)"; 

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

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

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

89 
by (parts_induct_tac 1); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

90 
(*NS3*) 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

91 
by (blast_tac (!claset addSEs partsEs) 3); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

92 
(*NS2*) 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

93 
by (blast_tac (!claset addSEs partsEs) 2); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

94 
by (Fake_parts_insert_tac 1); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

95 
qed "no_nonce_NS1_NS2"; 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

96 

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

97 

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

98 
(*Unicity for NS1: nonce NA identifies agents A and B*) 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

99 
goal thy 
3683  100 
"!!evs. [ Nonce NA ~: analz (spies evs); evs : ns_public ] \ 
3709  101 
\ ==> EX A' B'. ALL A B. \ 
3683  102 
\ Crypt (pubK B) {Nonce NA, Agent A} : parts (spies evs) > \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

103 
\ A=A' & B=B'"; 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

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

105 
by (parts_induct_tac 1); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

106 
by (ALLGOALS 
3683  107 
(asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_spies]))); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

108 
(*NS1*) 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

109 
by (expand_case_tac "NA = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

110 
(*Fake*) 
3709  111 
by (Clarify_tac 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

112 
by (ex_strip_tac 1); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

113 
by (Fake_parts_insert_tac 1); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

114 
val lemma = result(); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

115 

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

116 
goal thy 
3683  117 
"!!evs. [ Crypt(pubK B) {Nonce NA, Agent A} : parts(spies evs); \ 
118 
\ Crypt(pubK B') {Nonce NA, Agent A'} : parts(spies evs); \ 

119 
\ Nonce NA ~: analz (spies evs); \ 

3709  120 
\ evs : ns_public ] \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

121 
\ ==> A=A' & B=B'"; 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

122 
by (prove_unique_tac lemma 1); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

123 
qed "unique_NA"; 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

124 

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

125 

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

126 
(*Tactic for proving secrecy theorems*) 
2418
6b6a92d05fb2
New tactics: prove_unique_tac and analz_induct_tac
paulson
parents:
2374
diff
changeset

127 
fun analz_induct_tac i = 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

129 
ALLGOALS (asm_simp_tac 
3675
70dd312b70b2
Deleted the redundant simprule not_parts_not_analz
paulson
parents:
3545
diff
changeset

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

131 

2318  132 

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

134 
goal thy 

3709  135 
"!!evs. [ Says A B (Crypt(pubK B) {Nonce NA, Agent A}) : set evs; \ 
3683  136 
\ A ~: bad; B ~: bad; evs : ns_public ] \ 
137 
\ ==> Nonce NA ~: analz (spies evs)"; 

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

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

139 
by (analz_induct_tac 1); 
2318  140 
(*NS3*) 
3683  141 
by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj] 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

142 
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

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

144 
by (blast_tac (!claset addSEs [MPair_parts] 
3683  145 
addDs [Says_imp_spies RS parts.Inj, 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

146 
parts.Body, unique_NA]) 3); 
2318  147 
(*NS1*) 
3683  148 
by (blast_tac (!claset addSEs spies_partsEs 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

149 
addIs [impOfSubs analz_subset_parts]) 2); 
2318  150 
(*Fake*) 
2497  151 
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

152 
qed "Spy_not_see_NA"; 
2318  153 

154 

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

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

157 
goal thy 

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

158 
"!!evs. [ Says A B (Crypt (pubK B) {Nonce NA, Agent A}) : set evs; \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

159 
\ Says B' A (Crypt(pubK A) {Nonce NA, Nonce NB}): set evs; \ 
3709  160 
\ A ~: bad; B ~: bad; evs : ns_public ] \ 
3465  161 
\ ==> Says B A (Crypt(pubK A) {Nonce NA, Nonce NB}): set evs"; 
2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

162 
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

163 
(*prepare induction over Crypt (pubK A) {NA,NB} : parts H*) 
3683  164 
by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1); 
2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

165 
by (etac ns_public.induct 1); 
2318  166 
by (ALLGOALS Asm_simp_tac); 
3709  167 
by (ALLGOALS Clarify_tac); 
168 
(*NS2*) 

169 
by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, 

170 
Spy_not_see_NA, unique_NA]) 3); 

2318  171 
(*NS1*) 
3683  172 
by (blast_tac (!claset addSEs spies_partsEs) 2); 
2318  173 
(*Fake*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

174 
by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert] 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

175 
addDs [Spy_not_see_NA, 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

176 
impOfSubs analz_subset_parts]) 1); 
2318  177 
qed "A_trusts_NS2"; 
178 

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

180 
goal thy 

3683  181 
"!!evs. [ Crypt (pubK B) {Nonce NA, Agent A} : parts (spies evs); \ 
182 
\ Nonce NA ~: analz (spies evs); \ 

3709  183 
\ evs : ns_public ] \ 
3465  184 
\ ==> Says A B (Crypt (pubK B) {Nonce NA, Agent A}) : set evs"; 
2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

185 
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

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

187 
by (parts_induct_tac 1); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

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

189 
qed "B_trusts_NS1"; 
2318  190 

191 

192 

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

194 

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

3683  198 
"!!evs. [ Nonce NB ~: analz (spies evs); evs : ns_public ] \ 
3709  199 
\ ==> EX A' NA'. ALL A NA. \ 
200 
\ Crypt (pubK A) {Nonce NA, Nonce NB} \ 

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

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

203 
by (parts_induct_tac 1); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

204 
by (ALLGOALS 
3683  205 
(asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_spies]))); 
2318  206 
(*NS2*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

207 
by (expand_case_tac "NB = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2); 
2318  208 
(*Fake*) 
3709  209 
by (Clarify_tac 1); 
2318  210 
by (ex_strip_tac 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

211 
by (Fake_parts_insert_tac 1); 
2318  212 
val lemma = result(); 
213 

214 
goal thy 

3683  215 
"!!evs. [ Crypt(pubK A) {Nonce NA, Nonce NB} : parts(spies evs); \ 
216 
\ Crypt(pubK A'){Nonce NA', Nonce NB} : parts(spies evs); \ 

217 
\ Nonce NB ~: analz (spies evs); \ 

3709  218 
\ evs : ns_public ] \ 
2318  219 
\ ==> A=A' & NA=NA'"; 
2418
6b6a92d05fb2
New tactics: prove_unique_tac and analz_induct_tac
paulson
parents:
2374
diff
changeset

220 
by (prove_unique_tac lemma 1); 
2318  221 
qed "unique_NB"; 
222 

223 

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

225 
goal thy 

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

226 
"!!evs.[ Says B A (Crypt (pubK A) {Nonce NA, Nonce NB}) : set evs; \ 
3703  227 
\ ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set evs; \ 
228 
\ A ~: bad; B ~: bad; evs : ns_public ] \ 

3683  229 
\ ==> Nonce NB ~: analz (spies evs)"; 
2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

230 
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

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

232 
by (analz_induct_tac 1); 
3703  233 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); 
3709  234 
by (ALLGOALS Clarify_tac); 
3703  235 
(*NS3: because NB determines A*) 
236 
by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, unique_NB]) 4); 

237 
(*NS2: by freshness and unicity of NB*) 

238 
by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj] 

239 
addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)] 

240 
addEs partsEs 

241 
addIs [impOfSubs analz_subset_parts]) 3); 

242 
(*NS1: by freshness*) 

3683  243 
by (blast_tac (!claset addSEs spies_partsEs) 2); 
2318  244 
(*Fake*) 
2497  245 
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

246 
qed "Spy_not_see_NB"; 
2318  247 

248 

249 

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

251 
in message 2, then A has sent message 3to somebody....*) 
2318  252 
goal thy 
3545  253 
"!!evs. [ Says B A (Crypt (pubK A) {Nonce NA, Nonce NB}) : set evs; \ 
254 
\ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \ 

3683  255 
\ A ~: bad; B ~: bad; evs : ns_public ] \ 
3465  256 
\ ==> EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set evs"; 
2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

257 
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

258 
(*prepare induction over Crypt (pubK B) NB : parts H*) 
3683  259 
by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

260 
by (parts_induct_tac 1); 
2318  261 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); 
3709  262 
by (ALLGOALS Clarify_tac); 
3703  263 
(*NS3: because NB determines A*) 
264 
by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, 

265 
Spy_not_see_NB, unique_NB]) 3); 

266 
(*NS1: by freshness*) 

3683  267 
by (blast_tac (!claset addSEs spies_partsEs) 2); 
2318  268 
(*Fake*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

269 
by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert] 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

270 
addDs [Spy_not_see_NB, 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

271 
impOfSubs analz_subset_parts]) 1); 
2318  272 
qed "B_trusts_NS3"; 
273 

274 

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

276 
goal thy 

3683  277 
"!!evs. [ A ~: bad; B ~: bad; evs : ns_public ] \ 
3465  278 
\ ==> Says B A (Crypt (pubK A) {Nonce NA, Nonce NB}) : set evs \ 
3683  279 
\ > Nonce NB ~: analz (spies evs)"; 
2418
6b6a92d05fb2
New tactics: prove_unique_tac and analz_induct_tac
paulson
parents:
2374
diff
changeset

280 
by (analz_induct_tac 1); 
3709  281 
by (ALLGOALS Clarify_tac); 
3703  282 
(*NS2: by freshness and unicity of NB*) 
283 
by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj] 

284 
addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)] 

285 
addEs partsEs 

286 
addIs [impOfSubs analz_subset_parts]) 3); 

287 
(*NS1: by freshness*) 

288 
by (blast_tac (!claset addSEs spies_partsEs) 2); 

2318  289 
(*Fake*) 
2497  290 
by (spy_analz_tac 1); 
3703  291 
(*NS3: unicity of NB identifies A and NA, but not B*) 
3683  292 
by (forw_inst_tac [("A'","A")] (Says_imp_spies RS parts.Inj RS unique_NB) 1 
293 
THEN REPEAT (eresolve_tac [asm_rl, Says_imp_spies RS parts.Inj] 1)); 

3703  294 
by (Auto_tac()); 
295 
by (rename_tac "C B' evs3" 1); 

2318  296 

297 
(* 

298 
THIS IS THE ATTACK! 

3703  299 
Level 8 
3683  300 
!!evs. [ A ~: bad; B ~: bad; evs : ns_public ] 
3703  301 
==> Says B A (Crypt (pubK A) {Nonce NA, Nonce NB}) : set evs > 
3683  302 
Nonce NB ~: analz (spies evs) 
3703  303 
1. !!C B' evs3. 
304 
[ A ~: bad; B ~: bad; evs3 : ns_public; 

305 
Says A C (Crypt (pubK C) {Nonce NA, Agent A}) : set evs3; 

306 
Says B' A (Crypt (pubK A) {Nonce NA, Nonce NB}) : set evs3; C : bad; 

307 
Says B A (Crypt (pubK A) {Nonce NA, Nonce NB}) : set evs3; 

308 
Nonce NB ~: analz (spies evs3) ] 

2318  309 
==> False 
310 
*) 