author  paulson 
Fri, 11 Jul 1997 13:26:15 +0200  
changeset 3512  9dcb4daa15e8 
parent 3466  30791e5a69c4 
child 3519  ab0a9fbed4c0 
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 
(*A "possibility property": there are traces that reach the end*) 

26 
goal thy 

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

31 
by possibility_tac; 
2318  32 
result(); 
33 

34 

35 
(**** Inductive proofs about ns_public ****) 

36 

37 
(*Nobody sends themselves messages*) 

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

41 
qed_spec_mp "not_Says_to_self"; 

42 
Addsimps [not_Says_to_self]; 

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

44 

45 

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

47 
sends messages containing X! **) 

48 

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

50 
goal thy 

51 
"!!evs. evs : ns_public \ 

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

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

53 
by (etac ns_public.induct 1); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

54 
by (prove_simple_subgoals_tac 1); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

55 
by (Fake_parts_insert_tac 1); 
2318  56 
qed "Spy_see_priK"; 
57 
Addsimps [Spy_see_priK]; 

58 

59 
goal thy 

60 
"!!evs. evs : ns_public \ 

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

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

63 
qed "Spy_analz_priK"; 

64 
Addsimps [Spy_analz_priK]; 

65 

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

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

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

68 
by (blast_tac (!claset addDs [Spy_see_priK]) 1); 
2318  69 
qed "Spy_see_priK_D"; 
70 

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

72 
AddSDs [Spy_see_priK_D, Spy_analz_priK_D]; 

73 

74 

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

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

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

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

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

80 

2318  81 

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

83 

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

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

86 
goal thy 

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

87 
"!!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

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

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

90 
\ ==> 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

91 
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

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

93 
by (analz_induct_tac 1); 
2318  94 
(*NS3*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

95 
by (blast_tac (!claset addSEs partsEs) 4); 
2318  96 
(*NS2*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

97 
by (blast_tac (!claset addSEs partsEs) 3); 
2318  98 
(*Fake*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

100 
addDs [impOfSubs analz_subset_parts, 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

101 
impOfSubs Fake_parts_insert]) 2); 
2318  102 
(*Base*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

104 
qed "no_nonce_NS1_NS2"; 
2318  105 

106 

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

109 
"!!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

110 
\ ==> EX A' B'. ALL A B. \ 
2318  111 
\ 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

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

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

114 
by (analz_induct_tac 1); 
2318  115 
(*NS1*) 
2497  116 
by (simp_tac (!simpset addsimps [all_conj_distrib]) 3); 
2318  117 
by (expand_case_tac "NA = ?y" 3 THEN 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

118 
REPEAT (blast_tac (!claset addSEs partsEs) 3)); 
2318  119 
(*Base*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

120 
by (Blast_tac 1); 
2318  121 
(*Fake*) 
2497  122 
by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1); 
2374  123 
by (step_tac (!claset addSIs [analz_insertI]) 1); 
2318  124 
by (ex_strip_tac 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

125 
by (blast_tac (!claset delrules [conjI] 
3440
22db7a9cbb52
Deleted spurious reference to Spy_not_see_NB, which by chance was defined
paulson
parents:
3121
diff
changeset

126 
addSDs [impOfSubs Fake_parts_insert] 
22db7a9cbb52
Deleted spurious reference to Spy_not_see_NB, which by chance was defined
paulson
parents:
3121
diff
changeset

127 
addDs [impOfSubs analz_subset_parts]) 1); 
2318  128 
val lemma = result(); 
129 

130 
goal thy 

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

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

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

134 
\ evs : ns_public ] \ 

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

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

136 
by (prove_unique_tac lemma 1); 
2318  137 
qed "unique_NA"; 
138 

139 

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

141 
goal thy 

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

142 
"!!evs. [ 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

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

144 
\ ==> 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

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

146 
by (analz_induct_tac 1); 
2318  147 
(*NS3*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

148 
by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj] 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

149 
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

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

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

152 
addDs [Says_imp_sees_Spy' RS parts.Inj, 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

153 
parts.Body, unique_NA]) 3); 
2318  154 
(*NS1*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

155 
by (blast_tac (!claset addSEs sees_Spy_partsEs 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

156 
addIs [impOfSubs analz_subset_parts]) 2); 
2318  157 
(*Fake*) 
2497  158 
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

159 
qed "Spy_not_see_NA"; 
2318  160 

161 

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

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

164 
goal thy 

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

165 
"!!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

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

167 
\ A ~: lost; B ~: lost; evs : ns_public ] \ 
3465  168 
\ ==> 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

169 
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

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

171 
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

172 
by (etac ns_public.induct 1); 
2318  173 
by (ALLGOALS Asm_simp_tac); 
174 
(*NS1*) 

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

175 
by (blast_tac (!claset addSEs sees_Spy_partsEs) 2); 
2318  176 
(*Fake*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

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

179 
impOfSubs analz_subset_parts]) 1); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

180 
(*NS2; not clear why blast_tac needs to be preceeded by Step_tac*) 
2318  181 
by (Step_tac 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

182 
by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj, 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

183 
Spy_not_see_NA, unique_NA]) 1); 
2318  184 
qed "A_trusts_NS2"; 
185 

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

187 
goal thy 

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

188 
"!!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

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

190 
\ evs : ns_public ] \ 
3465  191 
\ ==> 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

192 
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

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

194 
by (analz_induct_tac 1); 
2318  195 
(*Fake*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

197 
addIs [analz_insertI] 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

198 
addDs [impOfSubs analz_subset_parts]) 2); 
2318  199 
(*Base*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

200 
by (Blast_tac 1); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

201 
qed "B_trusts_NS1"; 
2318  202 

203 

204 

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

206 

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

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

210 
"!!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

211 
\ ==> 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

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

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

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

215 
by (analz_induct_tac 1); 
2318  216 
(*NS2*) 
2497  217 
by (simp_tac (!simpset addsimps [all_conj_distrib]) 3); 
2318  218 
by (expand_case_tac "NB = ?y" 3 THEN 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

219 
REPEAT (blast_tac (!claset addSEs partsEs) 3)); 
2318  220 
(*Base*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

221 
by (Blast_tac 1); 
2318  222 
(*Fake*) 
2497  223 
by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1); 
2374  224 
by (step_tac (!claset addSIs [analz_insertI]) 1); 
2318  225 
by (ex_strip_tac 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

226 
by (blast_tac (!claset delrules [conjI] 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset

227 
addSDs [impOfSubs Fake_parts_insert] 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

228 
addDs [impOfSubs analz_subset_parts]) 1); 
2318  229 
val lemma = result(); 
230 

231 
goal thy 

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

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

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

235 
\ evs : ns_public ] \ 

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

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

237 
by (prove_unique_tac lemma 1); 
2318  238 
qed "unique_NB"; 
239 

240 

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

242 
goal thy 

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

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

244 
\ (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set evs); \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

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

246 
\ ==> 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

247 
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

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

249 
by (analz_induct_tac 1); 
2318  250 
(*NS1*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

251 
by (blast_tac (!claset addSEs sees_Spy_partsEs) 2); 
2318  252 
(*Fake*) 
2497  253 
by (spy_analz_tac 1); 
2318  254 
(*NS2 and NS3*) 
2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

255 
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

256 
by (step_tac (!claset delrules [allI]) 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

257 
by (Blast_tac 5); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

258 
(*NS3*) 
3440
22db7a9cbb52
Deleted spurious reference to Spy_not_see_NB, which by chance was defined
paulson
parents:
3121
diff
changeset

259 
by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj, unique_NB]) 4); 
2318  260 
(*NS2*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

261 
by (blast_tac (!claset addSEs sees_Spy_partsEs) 3); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

262 
by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

263 
addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

264 
by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts]) 1); 
2536
1e04eb7f7eb1
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents:
2516
diff
changeset

265 
qed "Spy_not_see_NB"; 
2318  266 

267 

268 

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

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

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

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

274 
\ Says A' B (Crypt (pubK B) (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

275 
\ A ~: lost; B ~: lost; evs : ns_public ] \ 
3465  276 
\ ==> 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

277 
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

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

279 
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

280 
by (analz_induct_tac 1); 
2318  281 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); 
282 
(*NS1*) 

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

283 
by (blast_tac (!claset addSEs sees_Spy_partsEs) 2); 
2318  284 
(*Fake*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

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

287 
impOfSubs analz_subset_parts]) 1); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

288 
(*NS3; not clear why blast_tac needs to be preceeded by Step_tac*) 
2318  289 
by (Step_tac 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

290 
by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj, 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

291 
Spy_not_see_NB, unique_NB]) 1); 
2318  292 
qed "B_trusts_NS3"; 
293 

294 

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

296 
goal thy 

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

297 
"!!evs. [ A ~: lost; B ~: lost; evs : ns_public ] \ 
3465  298 
\ ==> Says B A (Crypt (pubK A) {Nonce NA, Nonce NB}) : set evs \ 
2318  299 
\ > Nonce NB ~: analz (sees lost Spy evs)"; 
2418
6b6a92d05fb2
New tactics: prove_unique_tac and analz_induct_tac
paulson
parents:
2374
diff
changeset

300 
by (analz_induct_tac 1); 
2318  301 
(*NS1*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

302 
by (blast_tac (!claset addSEs partsEs 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

303 
addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2); 
2318  304 
(*Fake*) 
2497  305 
by (spy_analz_tac 1); 
2318  306 
(*NS2 and NS3*) 
307 
by (Step_tac 1); 

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

308 
by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts, usedI]) 1); 
2318  309 
(*NS2*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

310 
by (blast_tac (!claset addSEs partsEs 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

311 
addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

312 
by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

313 
addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1); 
2318  314 
(*NS3*) 
315 
by (forw_inst_tac [("A'","A")] (Says_imp_sees_Spy' RS parts.Inj RS unique_NB) 1 

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

317 
by (Step_tac 1); 

318 

319 
(* 

320 
THIS IS THE ATTACK! 

321 
Level 9 

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

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

3465  324 
: set evs > 
2318  325 
Nonce NB ~: analz (sees lost Spy evs) 
326 
1. !!evs Aa Ba B' NAa NBa evsa. 

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

3465  328 
Says B' A (Crypt (pubK A) {Nonce NA, Nonce NB}) : set evsa; 
329 
Says A Ba (Crypt (pubK Ba) {Nonce NA, Agent A}) : set evsa; 

2318  330 
Ba : lost; 
3465  331 
Says B A (Crypt (pubK A) {Nonce NA, Nonce NB}) : set evsa; 
2318  332 
Nonce NB ~: analz (sees lost Spy evsa) ] 
333 
==> False 

334 
*) 

335 

336 

337 