author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 9165  f46f407080f8 
child 10833  c0844a30ea4e 
permissions  rwrr 
1934  1 
(* Title: HOL/Auth/NS_Shared 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1996 University of Cambridge 

5 

6 
Inductive relation "ns_shared" for NeedhamSchroeder SharedKey protocol. 

7 

8 
From page 247 of 

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

10 
Proc. Royal Soc. 426 (1989) 

11 
*) 

12 

4470  13 
AddEs spies_partsEs; 
14 
AddDs [impOfSubs analz_subset_parts]; 

15 
AddDs [impOfSubs Fake_parts_insert]; 

16 

1997  17 

2323  18 
(*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

19 
Goal "[ A ~= Server ] \ 
4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

20 
\ ==> EX N K. EX evs: ns_shared. \ 
3465  21 
\ Says A B (Crypt K {Nonce N, Nonce N}) : set evs"; 
1997  22 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

23 
by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

24 
ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

25 
by possibility_tac; 
2015  26 
result(); 
27 

5278  28 
Goal "[ A ~= B; A ~= Server; B ~= Server ] \ 
3675
70dd312b70b2
Deleted the redundant simprule not_parts_not_analz
paulson
parents:
3651
diff
changeset

29 
\ ==> EX evs: ns_shared. \ 
70dd312b70b2
Deleted the redundant simprule not_parts_not_analz
paulson
parents:
3651
diff
changeset

30 
\ Says A B (Crypt ?K {Nonce ?N, Nonce ?N}) : set evs"; 
70dd312b70b2
Deleted the redundant simprule not_parts_not_analz
paulson
parents:
3651
diff
changeset

31 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
70dd312b70b2
Deleted the redundant simprule not_parts_not_analz
paulson
parents:
3651
diff
changeset

32 
by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS 
70dd312b70b2
Deleted the redundant simprule not_parts_not_analz
paulson
parents:
3651
diff
changeset

33 
ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2); 
70dd312b70b2
Deleted the redundant simprule not_parts_not_analz
paulson
parents:
3651
diff
changeset

34 
by possibility_tac; 
1943  35 

1934  36 
(**** Inductive proofs about ns_shared ****) 
37 

1943  38 
(*For reasoning about the encrypted portion of message NS3*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

39 
Goal "Says S A (Crypt KA {N, B, K, X}) : set evs \ 
3683  40 
\ ==> X : parts (spies evs)"; 
4470  41 
by (Blast_tac 1); 
3683  42 
qed "NS3_msg_in_parts_spies"; 
2032  43 

5278  44 
Goal "Says Server A (Crypt (shrK A) {NA, B, K, X}) : set evs \ 
3683  45 
\ ==> K : parts (spies evs)"; 
4470  46 
by (Blast_tac 1); 
3683  47 
qed "Oops_parts_spies"; 
2070  48 

3683  49 
(*For proving the easier theorems about X ~: parts (spies evs).*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

50 
fun parts_induct_tac i = 
4331  51 
EVERY [etac ns_shared.induct i, 
52 
REPEAT (FIRSTGOAL analz_mono_contra_tac), 

7499  53 
ftac Oops_parts_spies (i+7), 
54 
ftac NS3_msg_in_parts_spies (i+4), 

4331  55 
prove_simple_subgoals_tac i]; 
2070  56 

1934  57 

3683  58 
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY 
2015  59 
sends messages containing X! **) 
1934  60 

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

63 
by (parts_induct_tac 1); 
3961  64 
by (ALLGOALS Blast_tac); 
2131  65 
qed "Spy_see_shrK"; 
66 
Addsimps [Spy_see_shrK]; 

1934  67 

5278  68 
Goal "evs : ns_shared ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4470
diff
changeset

69 
by Auto_tac; 
2131  70 
qed "Spy_analz_shrK"; 
71 
Addsimps [Spy_analz_shrK]; 

1934  72 

4470  73 
AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
74 
Spy_analz_shrK RSN (2, rev_iffD1)]; 

1934  75 

2070  76 

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

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

78 
Goal "evs : ns_shared ==> \ 
3683  79 
\ Key K ~: used evs > K ~: keysFor (parts (spies evs))"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

82 
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

83 
(*NS2, NS4, NS5*) 
5054  84 
by (ALLGOALS Blast_tac); 
2160  85 
qed_spec_mp "new_keys_not_used"; 
1934  86 

87 
bind_thm ("new_keys_not_analzd", 

2032  88 
[analz_subset_parts RS keysFor_mono, 
89 
new_keys_not_used] MRS contra_subsetD); 

1934  90 

91 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 

92 

93 

94 
(** Lemmas concerning the form of items passed in messages **) 

95 

2015  96 
(*Describes the form of K, X and K' when the Server sends this message.*) 
5278  97 
Goal "[ Says Server A (Crypt K' {N, Agent B, Key K, X}) : set evs; \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

98 
\ evs : ns_shared ] \ 
4267  99 
\ ==> K ~: range shrK & \ 
100 
\ X = (Crypt (shrK B) {Key K, Agent A}) & \ 

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

101 
\ K' = shrK A"; 
2032  102 
by (etac rev_mp 1); 
103 
by (etac ns_shared.induct 1); 

4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4470
diff
changeset

104 
by Auto_tac; 
1934  105 
qed "Says_Server_message_form"; 
106 

107 

2070  108 
(*If the encrypted message appears then it originated with the Server*) 
5278  109 
Goal "[ Crypt (shrK A) {NA, Agent B, Key K, X} : parts (spies evs); \ 
4267  110 
\ A ~: bad; evs : ns_shared ] \ 
111 
\ ==> Says Server A (Crypt (shrK A) {NA, Agent B, Key K, X}) \ 

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

114 
by (parts_induct_tac 1); 
4470  115 
by (Blast_tac 1); 
2323  116 
qed "A_trusts_NS2"; 
1934  117 

1965  118 

5278  119 
Goal "[ Crypt (shrK A) {NA, Agent B, Key K, X} : parts (spies evs); \ 
4331  120 
\ A ~: bad; evs : ns_shared ] \ 
121 
\ ==> K ~: range shrK & X = (Crypt (shrK B) {Key K, Agent A})"; 

122 
by (blast_tac (claset() addSDs [A_trusts_NS2, Says_Server_message_form]) 1); 

123 
qed "cert_A_form"; 

124 

125 

1965  126 
(*EITHER describes the form of X when the following message is sent, 
127 
OR reduces it to the Fake case. 

128 
Use Says_Server_message_form if applicable.*) 

5278  129 
Goal "[ Says S A (Crypt (shrK A) {Nonce NA, Agent B, Key K, X}) \ 
3651  130 
\ : set evs; \ 
131 
\ evs : ns_shared ] \ 

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

132 
\ ==> (K ~: range shrK & X = (Crypt (shrK B) {Key K, Agent A})) \ 
3683  133 
\  X : analz (spies evs)"; 
134 
by (case_tac "A : bad" 1); 

4091  135 
by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj] 
4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

136 
addss (simpset())) 1); 
4470  137 
by (blast_tac (claset() addSDs [cert_A_form]) 1); 
1934  138 
qed "Says_S_message_form"; 
139 

140 

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

141 
(*For proofs involving analz.*) 
3683  142 
val analz_spies_tac = 
7499  143 
ftac Says_Server_message_form 8 THEN 
144 
ftac Says_S_message_form 5 THEN 

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

145 
REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac); 
2131  146 

1934  147 

148 
(**** 

149 
The following is to prove theorems of the form 

150 

3683  151 
Key K : analz (insert (Key KAB) (spies evs)) ==> 
152 
Key K : analz (spies evs) 

1934  153 

154 
A more general formula must be proved inductively. 

155 
****) 

156 

157 

158 
(*NOT useful in this form, but it says that session keys are not used 

159 
to encrypt messages containing other keys, in the actual protocol. 

160 
We require that agents should behave like this subsequently also.*) 

5278  161 
Goal "[ evs : ns_shared; Kab ~: range shrK ] ==> \ 
4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

162 
\ (Crypt KAB X) : parts (spies evs) & \ 
3683  163 
\ Key K : parts {X} > Key K : parts (spies evs)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

164 
by (parts_induct_tac 1); 
4470  165 
(*Fake*) 
4091  166 
by (blast_tac (claset() addSEs partsEs 
4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

167 
addDs [impOfSubs parts_insert_subset_Un]) 1); 
1965  168 
(*Base, NS4 and NS5*) 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4470
diff
changeset

169 
by Auto_tac; 
1934  170 
result(); 
171 

172 

173 
(** Session keys are not used to encrypt other session keys **) 

174 

2015  175 
(*The equality makes the induction hypothesis easier to apply*) 
5278  176 
Goal "evs : ns_shared ==> \ 
5492  177 
\ ALL K KK. KK <=  (range shrK) > \ 
3683  178 
\ (Key K : analz (Key``KK Un (spies evs))) = \ 
179 
\ (K : KK  Key K : analz (spies evs))"; 

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

182 
by (REPEAT_FIRST (resolve_tac [allI, impI])); 
3961  183 
by (REPEAT_FIRST (rtac analz_image_freshK_lemma)); 
184 
(*Takes 9 secs*) 

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

185 
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3441
diff
changeset

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

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

188 
qed_spec_mp "analz_image_freshK"; 
1934  189 

190 

5278  191 
Goal "[ evs : ns_shared; KAB ~: range shrK ] ==> \ 
3683  192 
\ Key K : analz (insert (Key KAB) (spies evs)) = \ 
193 
\ (K = KAB  Key K : analz (spies evs))"; 

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

194 
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:
2451
diff
changeset

195 
qed "analz_insert_freshK"; 
1934  196 

197 

2558  198 
(** The session key K uniquely identifies the message **) 
1965  199 

5278  200 
Goal "evs : ns_shared ==> \ 
4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

201 
\ EX A' NA' B' X'. ALL A NA B X. \ 
3683  202 
\ Says Server A (Crypt (shrK A) {NA, Agent B, Key K, X}) : set evs \ 
203 
\ > A=A' & NA=NA' & B=B' & X=X'"; 

2032  204 
by (etac ns_shared.induct 1); 
4091  205 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 
3730  206 
by Safe_tac; 
2070  207 
(*NS3*) 
208 
by (ex_strip_tac 2); 

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

209 
by (Blast_tac 2); 
2070  210 
(*NS2: it can't be a new key*) 
211 
by (expand_case_tac "K = ?y" 1); 

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

4470  213 
by (Blast_tac 1); 
1934  214 
val lemma = result(); 
215 

216 
(*In messages of this form, the session key uniquely identifies the rest*) 

5278  217 
Goal "[ Says Server A \ 
4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

218 
\ (Crypt (shrK A) {NA, Agent B, Key K, X}) : set evs; \ 
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

219 
\ Says Server A' \ 
3683  220 
\ (Crypt (shrK A') {NA', Agent B', Key K, X'}) : set evs; \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

221 
\ evs : ns_shared ] ==> A=A' & NA=NA' & B=B' & X = X'"; 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2374
diff
changeset

222 
by (prove_unique_tac lemma 1); 
1934  223 
qed "unique_session_keys"; 
224 

225 

2032  226 
(** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **) 
2015  227 

5278  228 
Goal "[ A ~: bad; B ~: bad; evs : ns_shared ] \ 
2015  229 
\ ==> Says Server A \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

230 
\ (Crypt (shrK A) {NA, Agent B, Key K, \ 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

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

232 
\ : set evs > \ 
4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

233 
\ (ALL NB. Notes Spy {NA, NB, Key K} ~: set evs) > \ 
3683  234 
\ Key K ~: analz (spies evs)"; 
2032  235 
by (etac ns_shared.induct 1); 
3683  236 
by analz_spies_tac; 
1934  237 
by (ALLGOALS 
2015  238 
(asm_simp_tac 
5535  239 
(simpset() addsimps [analz_insert_eq, analz_insert_freshK] @ 
240 
pushes @ split_ifs))); 

3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3441
diff
changeset

241 
(*Oops*) 
5480  242 
by (blast_tac (claset() addDs [unique_session_keys]) 5); 
3679  243 
(*NS3, replay subcase*) 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3441
diff
changeset

244 
by (Blast_tac 4); 
1934  245 
(*NS2*) 
4470  246 
by (Blast_tac 2); 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3441
diff
changeset

247 
(*Fake*) 
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3441
diff
changeset

248 
by (spy_analz_tac 1); 
3679  249 
(*NS3, Server subcase*) (**LEVEL 6 **) 
4091  250 
by (clarify_tac (claset() delrules [impCE]) 1); 
3683  251 
by (forward_tac [Says_imp_spies RS parts.Inj RS A_trusts_NS2] 1); 
2170  252 
by (assume_tac 2); 
4091  253 
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS 
4470  254 
Crypt_Spy_analz_bad]) 1); 
5480  255 
(*PROOF FAILED if addDs*) 
5453  256 
by (blast_tac (claset() addSDs [unique_session_keys]) 1); 
5480  257 
qed_spec_mp "lemma2"; 
2015  258 

259 

260 
(*Final version: Server's message in the most abstract form*) 

5278  261 
Goal "[ Says Server A \ 
4331  262 
\ (Crypt K' {NA, Agent B, Key K, X}) : set evs; \ 
4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

263 
\ ALL NB. Notes Spy {NA, NB, Key K} ~: set evs; \ 
3683  264 
\ A ~: bad; B ~: bad; evs : ns_shared \ 
265 
\ ] ==> Key K ~: analz (spies evs)"; 

7499  266 
by (ftac Says_Server_message_form 1 THEN assume_tac 1); 
5480  267 
by (blast_tac (claset() delrules [notI] 
268 
addIs [lemma2]) 1); 

2032  269 
qed "Spy_not_see_encrypted_key"; 
270 

271 

2070  272 
(**** Guarantees available at various stages of protocol ***) 
273 

3651  274 
A_trusts_NS2 RS Spy_not_see_encrypted_key; 
2070  275 

276 

277 
(*If the encrypted message appears then it originated with the Server*) 

5278  278 
Goal "[ Crypt (shrK B) {Key K, Agent A} : parts (spies evs); \ 
4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

279 
\ B ~: bad; evs : ns_shared ] \ 
2070  280 
\ ==> EX NA. Says Server A \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

281 
\ (Crypt (shrK A) {NA, Agent B, Key K, \ 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

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

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

286 
by (ALLGOALS Blast_tac); 
2323  287 
qed "B_trusts_NS3"; 
2070  288 

289 

5278  290 
Goal "[ Crypt K (Nonce NB) : parts (spies evs); \ 
4331  291 
\ Says Server A (Crypt (shrK A) {NA, Agent B, Key K, X}) \ 
292 
\ : set evs; \ 

293 
\ Key K ~: analz (spies evs); \ 

294 
\ evs : ns_shared ] \ 

295 
\ ==> Says B A (Crypt K (Nonce NB)) : set evs"; 

296 
by (etac rev_mp 1); 

297 
by (etac rev_mp 1); 

298 
by (etac rev_mp 1); 

299 
by (parts_induct_tac 1); 

4267  300 
(*NS3*) 
301 
by (Blast_tac 3); 

4470  302 
by (Blast_tac 1); 
4267  303 
(*NS2: contradiction from the assumptions 
4331  304 
Key K ~: used evs2 and Crypt K (Nonce NB) : parts (spies evs2) *) 
9165  305 
by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 
4331  306 
(**LEVEL 7**) 
307 
(*NS4*) 

308 
by (Clarify_tac 1); 

309 
by (not_bad_tac "Ba" 1); 

4470  310 
by (blast_tac (claset() addDs [B_trusts_NS3, unique_session_keys]) 1); 
4331  311 
qed "A_trusts_NS4_lemma"; 
2103  312 

4331  313 

314 
(*This version no longer assumes that K is secure*) 

5278  315 
Goal "[ Crypt K (Nonce NB) : parts (spies evs); \ 
4331  316 
\ Crypt (shrK A) {NA, Agent B, Key K, X} : parts (spies evs); \ 
4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

317 
\ ALL NB. Notes Spy {NA, NB, Key K} ~: set evs; \ 
4267  318 
\ A ~: bad; B ~: bad; evs : ns_shared ] \ 
3465  319 
\ ==> Says B A (Crypt K (Nonce NB)) : set evs"; 
4331  320 
by (blast_tac (claset() addSIs [A_trusts_NS2, A_trusts_NS4_lemma] 
9165  321 
addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1); 
2323  322 
qed "A_trusts_NS4"; 
4331  323 

324 

325 
(*If the session key has been used in NS4 then somebody has forwarded 

326 
component X in some instance of NS4. Perhaps an interesting property, 

327 
but not needed (after all) for the proofs below.*) 

5278  328 
Goal "[ Crypt K (Nonce NB) : parts (spies evs); \ 
4331  329 
\ Says Server A (Crypt (shrK A) {NA, Agent B, Key K, X}) \ 
330 
\ : set evs; \ 

331 
\ Key K ~: analz (spies evs); \ 

332 
\ evs : ns_shared ] \ 

333 
\ ==> EX A'. Says A' B X : set evs"; 

334 
by (etac rev_mp 1); 

335 
by (etac rev_mp 1); 

336 
by (etac rev_mp 1); 

337 
by (parts_induct_tac 1); 

338 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); 

339 
by (ALLGOALS Clarify_tac); 

4470  340 
by (Blast_tac 1); 
4331  341 
(**LEVEL 7**) 
342 
(*NS2*) 

343 
by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)] 

344 
addSDs [Crypt_imp_keysFor]) 1); 

345 
(*NS4*) 

346 
by (not_bad_tac "Ba" 1); 

347 
by (Asm_full_simp_tac 1); 

348 
by (forward_tac [Says_imp_spies RS parts.Inj RS B_trusts_NS3] 1); 

349 
by (ALLGOALS Clarify_tac); 

350 
by (blast_tac (claset() addDs [unique_session_keys]) 1); 

351 
qed "NS4_implies_NS3"; 

352 

353 

5278  354 
Goal "[ B ~: bad; evs : ns_shared ] \ 
4331  355 
\ ==> Key K ~: analz (spies evs) > \ 
5054  356 
\ Says Server A \ 
4331  357 
\ (Crypt (shrK A) {NA, Agent B, Key K, \ 
358 
\ Crypt (shrK B) {Key K, Agent A}}) \ 

5054  359 
\ : set evs > \ 
360 
\ Crypt K {Nonce NB, Nonce NB} : parts (spies evs) > \ 

4331  361 
\ Says A B (Crypt K {Nonce NB, Nonce NB}) : set evs"; 
362 
by (parts_induct_tac 1); 

363 
(*NS3*) 

4470  364 
by (blast_tac (claset() addSDs [cert_A_form]) 3); 
4331  365 
(*NS2*) 
366 
by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)] 

367 
addSDs [Crypt_imp_keysFor]) 2); 

4470  368 
by (Blast_tac 1); 
4331  369 
(**LEVEL 5**) 
370 
(*NS5*) 

371 
by (Clarify_tac 1); 

372 
by (not_bad_tac "Aa" 1); 

4470  373 
by (blast_tac (claset() addDs [A_trusts_NS2, unique_session_keys]) 1); 
5054  374 
qed_spec_mp "B_trusts_NS5_lemma"; 
4331  375 

376 

377 
(*Very strong Oops condition reveals protocol's weakness*) 

5278  378 
Goal "[ Crypt K {Nonce NB, Nonce NB} : parts (spies evs); \ 
4331  379 
\ Crypt (shrK B) {Key K, Agent A} : parts (spies evs); \ 
4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

380 
\ ALL NA NB. Notes Spy {NA, NB, Key K} ~: set evs; \ 
4331  381 
\ A ~: bad; B ~: bad; evs : ns_shared ] \ 
382 
\ ==> Says A B (Crypt K {Nonce NB, Nonce NB}) : set evs"; 

383 
by (dtac B_trusts_NS3 1); 

384 
by (ALLGOALS Clarify_tac); 

5054  385 
by (blast_tac (claset() addSIs [B_trusts_NS5_lemma] 
9165  386 
addDs [Spy_not_see_encrypted_key]) 1); 
4331  387 
qed "B_trusts_NS5"; 