author  paulson 
Thu, 08 Jan 1998 18:10:34 +0100  
changeset 4537  4e835bd9fada 
parent 4509  828148415197 
child 4598  649bf14debe7 
permissions  rwrr 
1941  1 
(* Title: HOL/Auth/OtwayRees 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1996 University of Cambridge 

5 

6 
Inductive relation "otway" for the OtwayRees protocol. 

7 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

8 
Version that encrypts Nonce NB 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

9 

1941  10 
From page 244 of 
11 
Burrows, Abadi and Needham. A Logic of Authentication. 

12 
Proc. Royal Soc. 426 (1989) 

13 
*) 

14 

15 
open OtwayRees; 

16 

4449  17 
set proof_timing; 
1941  18 
HOL_quantifiers := false; 
19 

4470  20 
AddEs spies_partsEs; 
21 
AddDs [impOfSubs analz_subset_parts]; 

22 
AddDs [impOfSubs Fake_parts_insert]; 

23 

1996
33c42cae3dd0
Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs
paulson
parents:
1967
diff
changeset

24 

2328  25 
(*A "possibility property": there are traces that reach the end*) 
1996
33c42cae3dd0
Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs
paulson
parents:
1967
diff
changeset

26 
goal thy 
33c42cae3dd0
Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs
paulson
parents:
1967
diff
changeset

27 
"!!A B. [ A ~= B; A ~= Server; B ~= Server ] \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

28 
\ ==> EX K. EX NA. EX evs: otway. \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

29 
\ Says B A {Nonce NA, Crypt (shrK A) {Nonce NA, Key K}} \ 
3465  30 
\ : set evs"; 
1996
33c42cae3dd0
Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs
paulson
parents:
1967
diff
changeset

31 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
2032  32 
by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

33 
by possibility_tac; 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

34 
result(); 
1996
33c42cae3dd0
Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs
paulson
parents:
1967
diff
changeset

35 

33c42cae3dd0
Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs
paulson
parents:
1967
diff
changeset

36 

1941  37 
(**** Inductive proofs about otway ****) 
38 

39 
(*Nobody sends themselves messages*) 

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

40 
goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs"; 
2032  41 
by (etac otway.induct 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4470
diff
changeset

42 
by Auto_tac; 
1941  43 
qed_spec_mp "not_Says_to_self"; 
44 
Addsimps [not_Says_to_self]; 

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

46 

47 

48 
(** For reasoning about the encrypted portion of messages **) 

49 

3465  50 
goal thy "!!evs. Says A' B {N, Agent A, Agent B, X} : set evs \ 
3683  51 
\ ==> X : analz (spies evs)"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4470
diff
changeset

52 
by (dtac (Says_imp_spies RS analz.Inj) 1); 
4470  53 
by (Blast_tac 1); 
3683  54 
qed "OR2_analz_spies"; 
1941  55 

3465  56 
goal thy "!!evs. Says S' B {N, X, Crypt (shrK B) X'} : set evs \ 
3683  57 
\ ==> X : analz (spies evs)"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4470
diff
changeset

58 
by (dtac (Says_imp_spies RS analz.Inj) 1); 
4470  59 
by (Blast_tac 1); 
3683  60 
qed "OR4_analz_spies"; 
1941  61 

3465  62 
goal thy "!!evs. Says Server B {NA, X, Crypt K' {NB,K}} : set evs \ 
4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

63 
\ ==> K : parts (spies evs)"; 
4470  64 
by (Blast_tac 1); 
3683  65 
qed "Oops_parts_spies"; 
1941  66 

3683  67 
bind_thm ("OR2_parts_spies", 
68 
OR2_analz_spies RS (impOfSubs analz_subset_parts)); 

69 
bind_thm ("OR4_parts_spies", 

70 
OR4_analz_spies RS (impOfSubs analz_subset_parts)); 

2032  71 

3683  72 
(*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

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

74 
etac otway.induct i THEN 
3683  75 
forward_tac [Oops_parts_spies] (i+6) THEN 
76 
forward_tac [OR4_parts_spies] (i+5) THEN 

77 
forward_tac [OR2_parts_spies] (i+3) THEN 

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

78 
prove_simple_subgoals_tac i; 
1941  79 

80 

3683  81 
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

82 
sends messages containing X! **) 
1941  83 

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

84 
(*Spy never sees a good agent's shared key!*) 
1941  85 
goal thy 
3683  86 
"!!evs. evs : otway ==> (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

87 
by (parts_induct_tac 1); 
3961  88 
by (ALLGOALS Blast_tac); 
2135  89 
qed "Spy_see_shrK"; 
90 
Addsimps [Spy_see_shrK]; 

1941  91 

2135  92 
goal thy 
3683  93 
"!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; 
4091  94 
by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); 
2135  95 
qed "Spy_analz_shrK"; 
96 
Addsimps [Spy_analz_shrK]; 

1941  97 

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

1941  100 

101 

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

102 
(*Nobody can have used nonexistent keys!*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

103 
goal thy "!!evs. evs : otway ==> \ 
3683  104 
\ 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

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

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

107 
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); 
4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

108 
(*OR2, OR3*) 
3102  109 
by (ALLGOALS Blast_tac); 
2160  110 
qed_spec_mp "new_keys_not_used"; 
1941  111 

112 
bind_thm ("new_keys_not_analzd", 

2032  113 
[analz_subset_parts RS keysFor_mono, 
114 
new_keys_not_used] MRS contra_subsetD); 

1941  115 

116 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 

117 

118 

2064  119 

120 
(*** Proofs involving analz ***) 

121 

2135  122 
(*Describes the form of K and NA when the Server sends this message. Also 
123 
for Oops case.*) 

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

125 
"!!evs. [ Says Server B {NA, X, Crypt (shrK B) {NB, Key K}} : set evs; \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

127 
\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; 
2135  128 
by (etac rev_mp 1); 
129 
by (etac otway.induct 1); 

3102  130 
by (ALLGOALS Simp_tac); 
131 
by (ALLGOALS Blast_tac); 

2135  132 
qed "Says_Server_message_form"; 
2064  133 

134 

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

135 
(*For proofs involving analz.*) 
3683  136 
val analz_spies_tac = 
137 
dtac OR2_analz_spies 4 THEN 

138 
dtac OR4_analz_spies 6 THEN 

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

139 
forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2417
diff
changeset

140 
REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7); 
1941  141 

142 

143 
(**** 

144 
The following is to prove theorems of the form 

145 

3683  146 
Key K : analz (insert (Key KAB) (spies evs)) ==> 
147 
Key K : analz (spies evs) 

1941  148 

149 
A more general formula must be proved inductively. 

150 
****) 

151 

152 

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

154 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

155 
(*The equality makes the induction hypothesis easier to apply*) 
1941  156 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

157 
"!!evs. evs : otway ==> \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

158 
\ ALL K KK. KK <= Compl (range shrK) > \ 
3683  159 
\ (Key K : analz (Key``KK Un (spies evs))) = \ 
160 
\ (K : KK  Key K : analz (spies evs))"; 

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

163 
by (REPEAT_FIRST (resolve_tac [allI, impI])); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

164 
by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

165 
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:
3207
diff
changeset

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

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

168 
qed_spec_mp "analz_image_freshK"; 
1941  169 

170 

171 
goal thy 

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

172 
"!!evs. [ evs : otway; KAB ~: range shrK ] ==> \ 
3683  173 
\ Key K : analz (insert (Key KAB) (spies evs)) = \ 
174 
\ (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

175 
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

176 
qed "analz_insert_freshK"; 
1941  177 

178 

2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2014
diff
changeset

179 
(*** The Key K uniquely identifies the Server's message. **) 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

180 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

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

182 
"!!evs. evs : otway ==> \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

183 
\ EX B' NA' NB' X'. ALL B NA NB X. \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

184 
\ Says Server B {NA, X, Crypt (shrK B) {NB, K}} : set evs > \ 
2135  185 
\ B=B' & NA=NA' & NB=NB' & X=X'"; 
2032  186 
by (etac otway.induct 1); 
4091  187 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 
3730  188 
by (ALLGOALS Clarify_tac); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

189 
(*Remaining cases: OR3 and OR4*) 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

190 
by (ex_strip_tac 2); 
4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

191 
by (Best_tac 2); (*Blast_tac's too slow (in reconstruction)*) 
2064  192 
by (expand_case_tac "K = ?y" 1); 
193 
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); 

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

194 
(*...we assume X is a recent message, and handle this case by contradiction*) 
4509
828148415197
Making proofs faster, especially using keysFor_parts_insert
paulson
parents:
4477
diff
changeset

195 
by (blast_tac (claset() addSEs spies_partsEs) 1); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

196 
val lemma = result(); 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

197 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

198 
goal thy 
3543  199 
"!!evs. [ Says Server B {NA, X, Crypt (shrK B) {NB, K}} : set evs; \ 
200 
\ Says Server B' {NA',X',Crypt (shrK B') {NB',K}} : set evs; \ 

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

201 
\ evs : otway ] ==> X=X' & B=B' & NA=NA' & NB=NB'"; 
2417  202 
by (prove_unique_tac lemma 1); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

203 
qed "unique_session_keys"; 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

204 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

205 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

206 

2048  207 
(**** Authenticity properties relating to NA ****) 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

208 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

209 
(*Only OR1 can have caused such a part of a message to appear.*) 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

210 
goal thy 
3683  211 
"!!evs. [ A ~: bad; evs : otway ] \ 
212 
\ ==> Crypt (shrK A) {NA, Agent A, Agent B} : parts (spies evs) > \ 

2064  213 
\ Says A B {NA, Agent A, Agent B, \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

214 
\ Crypt (shrK A) {NA, Agent A, Agent B}} \ 
3465  215 
\ : set evs"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

216 
by (parts_induct_tac 1); 
4470  217 
by (Blast_tac 1); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

218 
qed_spec_mp "Crypt_imp_OR1"; 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

219 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

220 

2064  221 
(** The Nonce NA uniquely identifies A's message. **) 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

222 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

223 
goal thy 
3683  224 
"!!evs. [ evs : otway; A ~: bad ] \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

225 
\ ==> EX B'. ALL B. \ 
3683  226 
\ Crypt (shrK A) {NA, Agent A, Agent B} : parts (spies evs) \ 
2048  227 
\ > B = B'"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

228 
by (parts_induct_tac 1); 
4470  229 
by (Blast_tac 1); 
4091  230 
by (simp_tac (simpset() addsimps [all_conj_distrib]) 1); 
2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2014
diff
changeset

231 
(*OR1: creation of new Nonce. Move assertion into global context*) 
2064  232 
by (expand_case_tac "NA = ?y" 1); 
4470  233 
by (Blast_tac 1); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

234 
val lemma = result(); 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

235 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

236 
goal thy 
3683  237 
"!!evs.[ Crypt (shrK A) {NA, Agent A, Agent B}: parts (spies evs); \ 
238 
\ Crypt (shrK A) {NA, Agent A, Agent C}: parts (spies evs); \ 

239 
\ evs : otway; A ~: bad ] \ 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

240 
\ ==> B = C"; 
2417  241 
by (prove_unique_tac lemma 1); 
2048  242 
qed "unique_NA"; 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

243 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

244 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

245 
(*It is impossible to reuse a nonce in both OR1 and OR2. This holds because 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

246 
OR2 encrypts Nonce NB. It prevents the attack that can occur in the 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

247 
oversimplified version of this protocol: see OtwayRees_Bad.*) 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

248 
goal thy 
3683  249 
"!!evs. [ A ~: bad; evs : otway ] \ 
250 
\ ==> Crypt (shrK A) {NA, Agent A, Agent B} : parts (spies evs) > \ 

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

251 
\ Crypt (shrK A) {NA', NA, Agent A', Agent A} \ 
3683  252 
\ ~: parts (spies evs)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

253 
by (parts_induct_tac 1); 
4470  254 
by (ALLGOALS Blast_tac); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

255 
qed_spec_mp"no_nonce_OR1_OR2"; 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

256 

4470  257 
val nonce_OR1_OR2_E = no_nonce_OR1_OR2 RSN (2, rev_notE); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

258 

2053  259 
(*Crucial property: If the encrypted message appears, and A has used NA 
260 
to start a run, then it originated with the Server!*) 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

261 
goal thy 
3683  262 
"!!evs. [ A ~: bad; A ~= Spy; evs : otway ] \ 
263 
\ ==> Crypt (shrK A) {NA, Key K} : parts (spies evs) \ 

2048  264 
\ > Says A B {NA, Agent A, Agent B, \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

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

266 
\ : set evs > \ 
2048  267 
\ (EX NB. Says Server B \ 
268 
\ {NA, \ 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

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

270 
\ Crypt (shrK B) {NB, Key K}} \ 
3465  271 
\ : set evs)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

272 
by (parts_induct_tac 1); 
4470  273 
by (Blast_tac 1); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

274 
(*OR1: it cannot be a new Nonce, contradiction.*) 
4470  275 
by (Blast_tac 1); 
3730  276 
(*OR3 and OR4*) 
4091  277 
by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1); 
3730  278 
by (rtac conjI 1); 
279 
by (ALLGOALS Clarify_tac); 

280 
(*OR4*) 

4470  281 
by (blast_tac (claset() addSIs [Crypt_imp_OR1]) 3); 
282 
(*OR3, two cases*) (** LEVEL 7 **) 

283 
by (blast_tac (claset() addSEs [nonce_OR1_OR2_E] 

284 
delrules [conjI] (*stop splitup into 4 subgoals*)) 2); 

285 
by (blast_tac (claset() addIs [unique_NA]) 1); 

2048  286 
qed_spec_mp "NA_Crypt_imp_Server_msg"; 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

287 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

288 

2053  289 
(*Corollary: if A receives B's OR4 message and the nonce NA agrees 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

290 
then the key really did come from the Server! CANNOT prove this of the 
2048  291 
bad form of this protocol, even though we can prove 
2032  292 
Spy_not_see_encrypted_key*) 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

293 
goal thy 
3683  294 
"!!evs. [ Says B' A {NA, Crypt (shrK A) {NA, Key K}} : set evs; \ 
295 
\ Says A B {NA, Agent A, Agent B, \ 

296 
\ Crypt (shrK A) {NA, Agent A, Agent B}} : set evs; \ 

297 
\ A ~: bad; A ~= Spy; evs : otway ] \ 

2053  298 
\ ==> EX NB. Says Server B \ 
2048  299 
\ {NA, \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

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

301 
\ Crypt (shrK B) {NB, Key K}} \ 
3465  302 
\ : set evs"; 
4470  303 
by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1); 
2328  304 
qed "A_trusts_OR4"; 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

305 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

306 

2048  307 
(** Crucial secrecy property: Spy does not see the keys sent in msg OR3 
308 
Does not in itself guarantee security: an attack could violate 

309 
the premises, e.g. by having A=Spy **) 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

310 

1941  311 
goal thy 
4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

312 
"!!evs. [ A ~: bad; B ~: bad; evs : otway ] \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

313 
\ ==> Says Server B \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

314 
\ {NA, Crypt (shrK A) {NA, Key K}, \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

315 
\ Crypt (shrK B) {NB, Key K}} : set evs > \ 
4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

316 
\ Notes Spy {NA, NB, Key K} ~: set evs > \ 
3683  317 
\ Key K ~: analz (spies evs)"; 
2032  318 
by (etac otway.induct 1); 
3683  319 
by analz_spies_tac; 
1964  320 
by (ALLGOALS 
4091  321 
(asm_simp_tac (simpset() addcongs [conj_cong] 
4509
828148415197
Making proofs faster, especially using keysFor_parts_insert
paulson
parents:
4477
diff
changeset

322 
addsimps [analz_insert_eq, analz_insert_freshK] 
828148415197
Making proofs faster, especially using keysFor_parts_insert
paulson
parents:
4477
diff
changeset

323 
addsimps (pushes@expand_ifs)))); 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

324 
(*Oops*) 
4091  325 
by (blast_tac (claset() addSDs [unique_session_keys]) 4); 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

326 
(*OR4*) 
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

327 
by (Blast_tac 3); 
1941  328 
(*OR3*) 
4470  329 
by (Blast_tac 2); 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

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

331 
by (spy_analz_tac 1); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

332 
val lemma = result() RS mp RS mp RSN(2,rev_notE); 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

333 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

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

335 
"!!evs. [ Says Server B \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

336 
\ {NA, Crypt (shrK A) {NA, Key K}, \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

337 
\ Crypt (shrK B) {NB, Key K}} : set evs; \ 
4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

338 
\ Notes Spy {NA, NB, Key K} ~: set evs; \ 
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

339 
\ A ~: bad; B ~: bad; evs : otway ] \ 
3683  340 
\ ==> Key K ~: analz (spies evs)"; 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

341 
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); 
4091  342 
by (blast_tac (claset() addSEs [lemma]) 1); 
2032  343 
qed "Spy_not_see_encrypted_key"; 
344 

1945  345 

2048  346 
(**** Authenticity properties relating to NB ****) 
347 

348 
(*Only OR2 can have caused such a part of a message to appear. We do not 

2194
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

349 
know anything about X: it does NOT have to have the right form.*) 
2048  350 
goal thy 
3683  351 
"!!evs. [ B ~: bad; evs : otway ] \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

352 
\ ==> Crypt (shrK B) {NA, NB, Agent A, Agent B} \ 
3683  353 
\ : parts (spies evs) > \ 
2194
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

354 
\ (EX X. Says B Server \ 
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

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

356 
\ Crypt (shrK B) {NA, NB, Agent A, Agent B}} \ 
3465  357 
\ : set evs)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

358 
by (parts_induct_tac 1); 
3102  359 
by (ALLGOALS Blast_tac); 
2194
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

360 
bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE); 
2048  361 

362 

363 
(** The Nonce NB uniquely identifies B's message. **) 

364 

365 
goal thy 

3683  366 
"!!evs. [ evs : otway; B ~: bad ] \ 
2064  367 
\ ==> EX NA' A'. ALL NA A. \ 
3683  368 
\ Crypt (shrK B) {NA, NB, Agent A, Agent B} : parts(spies evs) \ 
2048  369 
\ > NA = NA' & A = A'"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

370 
by (parts_induct_tac 1); 
4470  371 
by (Blast_tac 1); 
4091  372 
by (simp_tac (simpset() addsimps [all_conj_distrib]) 1); 
2048  373 
(*OR2: creation of new Nonce. Move assertion into global context*) 
2064  374 
by (expand_case_tac "NB = ?y" 1); 
4470  375 
by (Blast_tac 1); 
2048  376 
val lemma = result(); 
377 

378 
goal thy 

3683  379 
"!!evs.[ Crypt (shrK B) {NA, NB, Agent A, Agent B} : parts(spies evs); \ 
380 
\ Crypt (shrK B) {NC, NB, Agent C, Agent B} : parts(spies evs); \ 

381 
\ evs : otway; B ~: bad ] \ 

2048  382 
\ ==> NC = NA & C = A"; 
2417  383 
by (prove_unique_tac lemma 1); 
2048  384 
qed "unique_NB"; 
385 

386 

387 
(*If the encrypted message appears, and B has used Nonce NB, 

388 
then it originated with the Server!*) 

389 
goal thy 

3683  390 
"!!evs. [ B ~: bad; B ~= Spy; evs : otway ] \ 
391 
\ ==> Crypt (shrK B) {NB, Key K} : parts (spies evs) \ 

2048  392 
\ > (ALL X'. Says B Server \ 
393 
\ {NA, Agent A, Agent B, X', \ 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

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

395 
\ : set evs \ 
2048  396 
\ > Says Server B \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

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

398 
\ Crypt (shrK B) {NB, Key K}} \ 
3465  399 
\ : set evs)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

400 
by (parts_induct_tac 1); 
4470  401 
by (Blast_tac 1); 
2048  402 
(*OR1: it cannot be a new Nonce, contradiction.*) 
4470  403 
by (Blast_tac 1); 
2048  404 
(*OR4*) 
4470  405 
by (blast_tac (claset() addSEs [Crypt_imp_OR2]) 2); 
2194
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

406 
(*OR3*) 
4470  407 
(*Provable in 38s by the single command 
408 
by (blast_tac (claset() addDs [unique_NB] addEs[nonce_OR1_OR2_E]) 1); 

409 
*) 

4091  410 
by (safe_tac (claset() delrules [disjCI, impCE])); 
4470  411 
by (Blast_tac 3); 
412 
by (blast_tac (claset() addDs [unique_NB]) 2); 

413 
by (blast_tac (claset() addSEs [nonce_OR1_OR2_E] 

414 
delrules [conjI] (*stop splitup*)) 1); 

2048  415 
qed_spec_mp "NB_Crypt_imp_Server_msg"; 
416 

417 

418 
(*Guarantee for B: if it gets a message with matching NB then the Server 

419 
has sent the correct message.*) 

420 
goal thy 

3683  421 
"!!evs. [ B ~: bad; B ~= Spy; evs : otway; \ 
422 
\ Says S' B {NA, X, Crypt (shrK B) {NB, Key K}} : set evs; \ 

2048  423 
\ Says B Server {NA, Agent A, Agent B, X', \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

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

425 
\ : set evs ] \ 
2048  426 
\ ==> Says Server B \ 
427 
\ {NA, \ 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

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

429 
\ Crypt (shrK B) {NB, Key K}} \ 
3465  430 
\ : set evs"; 
4470  431 
by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1); 
2328  432 
qed "B_trusts_OR3"; 
2048  433 

434 

2328  435 
B_trusts_OR3 RS Spy_not_see_encrypted_key; 
2048  436 

437 

1945  438 
goal thy 
3683  439 
"!!evs. [ B ~: bad; evs : otway ] \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

440 
\ ==> Says Server B \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

441 
\ {NA, Crypt (shrK A) {NA, Key K}, \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

442 
\ Crypt (shrK B) {NB, Key K}} : set evs > \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

443 
\ (EX X. Says B Server {NA, Agent A, Agent B, X, \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

444 
\ Crypt (shrK B) {NA, NB, Agent A, Agent B} } \ 
3465  445 
\ : set evs)"; 
2032  446 
by (etac otway.induct 1); 
3102  447 
by (ALLGOALS Asm_simp_tac); 
4470  448 
by (blast_tac (claset() addSEs [Crypt_imp_OR2]) 3); 
3102  449 
by (ALLGOALS Blast_tac); 
2194
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

450 
bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE); 
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

451 

63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

452 

63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

453 
(*After getting and checking OR4, agent A can trust that B has been active. 
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

454 
We could probably prove that X has the expected form, but that is not 
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

455 
strictly necessary for authentication.*) 
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

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

457 
"!!evs. [ Says B' A {NA, Crypt (shrK A) {NA, Key K}} : set evs; \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

458 
\ Says A B {NA, Agent A, Agent B, \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

459 
\ Crypt (shrK A) {NA, Agent A, Agent B}} : set evs; \ 
3683  460 
\ A ~: bad; A ~= Spy; B ~: bad; evs : otway ] \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

461 
\ ==> EX NB X. Says B Server {NA, Agent A, Agent B, X, \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

462 
\ Crypt (shrK B) {NA, NB, Agent A, Agent B} }\ 
3465  463 
\ : set evs"; 
4470  464 
by (blast_tac (claset() addSDs [A_trusts_OR4] 
465 
addSEs [OR3_imp_OR2]) 1); 

2194
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

466 
qed "A_auths_B"; 