author  paulson 
Fri, 11 Jul 1997 13:26:15 +0200  
changeset 3512  9dcb4daa15e8 
parent 3466  30791e5a69c4 
child 3516  470626799511 
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 

17 
proof_timing:=true; 

18 
HOL_quantifiers := false; 

19 

3102  20 
(*Replacing the variable by a constant improves search speed by 50%!*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

21 
val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy; 
3102  22 

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

23 

2328  24 
(*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

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

26 
"!!A B. [ A ~= B; A ~= Server; B ~= Server ] \ 
2032  27 
\ ==> EX K. EX NA. EX evs: otway lost. \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

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

30 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
2032  31 
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

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

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

34 

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

35 

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

2104
f5c9a91e4b50
Replaced excluded_middle_tac by case_tac; tidied proofs
paulson
parents:
2071
diff
changeset

38 
(*Monotonicity*) 
2032  39 
goal thy "!!evs. lost' <= lost ==> otway lost' <= otway lost"; 
40 
by (rtac subsetI 1); 

41 
by (etac otway.induct 1); 

3102  42 
by (ALLGOALS 
43 
(blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono) 

2032  44 
:: otway.intrs)))); 
45 
qed "otway_mono"; 

46 

1941  47 
(*Nobody sends themselves messages*) 
3465  48 
goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set evs"; 
2032  49 
by (etac otway.induct 1); 
1941  50 
by (Auto_tac()); 
51 
qed_spec_mp "not_Says_to_self"; 

52 
Addsimps [not_Says_to_self]; 

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

54 

55 

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

57 

3465  58 
goal thy "!!evs. Says A' B {N, Agent A, Agent B, X} : set evs \ 
2135  59 
\ ==> X : analz (sees lost Spy evs)"; 
3102  60 
by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1); 
2032  61 
qed "OR2_analz_sees_Spy"; 
1941  62 

3465  63 
goal thy "!!evs. Says S' B {N, X, Crypt (shrK B) X'} : set evs \ 
2135  64 
\ ==> X : analz (sees lost Spy evs)"; 
3102  65 
by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1); 
2032  66 
qed "OR4_analz_sees_Spy"; 
1941  67 

3465  68 
goal thy "!!evs. Says Server B {NA, X, Crypt K' {NB,K}} : set evs \ 
2135  69 
\ ==> K : parts (sees lost Spy evs)"; 
3102  70 
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); 
2135  71 
qed "Oops_parts_sees_Spy"; 
1941  72 

73 
(*OR2_analz... and OR4_analz... let us treat those cases using the same 

1964  74 
argument as for the Fake case. This is possible for most, but not all, 
75 
proofs: Fake does not invent new nonces (as in OR2), and of course Fake 

2032  76 
messages originate from the Spy. *) 
1964  77 

2032  78 
bind_thm ("OR2_parts_sees_Spy", 
79 
OR2_analz_sees_Spy RS (impOfSubs analz_subset_parts)); 

80 
bind_thm ("OR4_parts_sees_Spy", 

81 
OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); 

82 

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

83 
(*For proving the easier theorems about X ~: parts (sees lost Spy evs). 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

84 
We instantiate the variable to "lost" since leaving it as a Var would 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

85 
interfere with simplification.*) 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

86 
val parts_induct_tac = 
2032  87 
let val tac = forw_inst_tac [("lost","lost")] 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

88 
in etac otway.induct 1 THEN 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

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

90 
tac OR4_parts_sees_Spy 6 THEN 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

91 
tac Oops_parts_sees_Spy 7 THEN 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

92 
prove_simple_subgoals_tac 1 
2032  93 
end; 
1941  94 

95 

2032  96 
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

97 
sends messages containing X! **) 
1941  98 

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

99 

2064  100 
(*Spy never sees another agent's shared key! (unless it's lost at start)*) 
1941  101 
goal thy 
2135  102 
"!!evs. evs : otway lost \ 
103 
\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; 

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

104 
by parts_induct_tac; 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

105 
by (Fake_parts_insert_tac 1); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

106 
by (Blast_tac 1); 
2135  107 
qed "Spy_see_shrK"; 
108 
Addsimps [Spy_see_shrK]; 

1941  109 

2135  110 
goal thy 
111 
"!!evs. evs : otway lost \ 

112 
\ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)"; 

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

114 
qed "Spy_analz_shrK"; 

115 
Addsimps [Spy_analz_shrK]; 

1941  116 

2135  117 
goal thy "!!A. [ Key (shrK A) : parts (sees lost Spy evs); \ 
118 
\ evs : otway lost ] ==> A:lost"; 

3102  119 
by (blast_tac (!claset addDs [Spy_see_shrK]) 1); 
2135  120 
qed "Spy_see_shrK_D"; 
1941  121 

2135  122 
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); 
123 
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; 

1941  124 

125 

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

126 
(*Nobody can have used nonexistent keys!*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

127 
goal thy "!!evs. evs : otway lost ==> \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

128 
\ Key K ~: used evs > K ~: keysFor (parts (sees lost Spy evs))"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

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

130 
(*Fake*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

132 
(!claset addIs [impOfSubs analz_subset_parts] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

133 
addDs [impOfSubs (analz_subset_parts RS keysFor_mono), 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

134 
impOfSubs (parts_insert_subset_Un RS keysFor_mono)] 
3207  135 
addss (!simpset)) 1); 
3102  136 
by (ALLGOALS Blast_tac); 
2160  137 
qed_spec_mp "new_keys_not_used"; 
1941  138 

139 
bind_thm ("new_keys_not_analzd", 

2032  140 
[analz_subset_parts RS keysFor_mono, 
141 
new_keys_not_used] MRS contra_subsetD); 

1941  142 

143 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 

144 

145 

2064  146 

147 
(*** Proofs involving analz ***) 

148 

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

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

152 
"!!evs. [ Says Server B \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

153 
\ {NA, X, Crypt (shrK B) {NB, Key K}} : set evs; \ 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2417
diff
changeset

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

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

3102  158 
by (ALLGOALS Simp_tac); 
159 
by (ALLGOALS Blast_tac); 

2135  160 
qed "Says_Server_message_form"; 
2064  161 

162 

163 
(*For proofs involving analz. We again instantiate the variable to "lost".*) 

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

164 
val analz_sees_tac = 
2064  165 
dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4 THEN 
166 
dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN 

2135  167 
forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

168 
assume_tac 7 THEN 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2417
diff
changeset

169 
REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7); 
1941  170 

171 

172 
(**** 

173 
The following is to prove theorems of the form 

174 

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

175 
Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==> 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2417
diff
changeset

176 
Key K : analz (sees lost Spy evs) 
1941  177 

178 
A more general formula must be proved inductively. 

179 
****) 

180 

181 

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

183 

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

184 
(*The equality makes the induction hypothesis easier to apply*) 
1941  185 
goal thy 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

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

187 
\ ALL K KK. KK <= Compl (range shrK) > \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

188 
\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

189 
\ (K : KK  Key K : analz (sees lost Spy evs))"; 
2032  190 
by (etac otway.induct 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

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

192 
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

193 
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

194 
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

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

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

197 
(*Base*) 
3102  198 
by (Blast_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

199 
qed_spec_mp "analz_image_freshK"; 
1941  200 

201 

202 
goal thy 

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

203 
"!!evs. [ evs : otway lost; KAB ~: range shrK ] ==> \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

204 
\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

205 
\ (K = KAB  Key K : analz (sees lost Spy evs))"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

206 
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

207 
qed "analz_insert_freshK"; 
1941  208 

209 

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

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

211 

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

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

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

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

215 
\ Says Server B {NA, X, Crypt (shrK B) {NB, K}} : set evs > \ 
2135  216 
\ B=B' & NA=NA' & NB=NB' & X=X'"; 
2032  217 
by (etac otway.induct 1); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

218 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

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

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

221 
by (ex_strip_tac 2); 
3102  222 
by (Best_tac 2); 
2064  223 
by (expand_case_tac "K = ?y" 1); 
224 
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

225 
(*...we assume X is a recent message, and handle this case by contradiction*) 
3102  226 
by (blast_tac (!claset addSEs sees_Spy_partsEs 
227 
delrules [conjI] (*no splitup into 4 subgoals*)) 1); 

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

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

229 

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

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

231 
"!!evs. [ Says Server B {NA, X, Crypt (shrK B) {NB, K}} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

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

233 
\ Says Server B' {NA',X',Crypt (shrK B') {NB',K}} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

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

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

238 

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

239 

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

240 

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

242 

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

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

244 
goal thy 
2064  245 
"!!evs. [ A ~: lost; evs : otway lost ] \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

246 
\ ==> Crypt (shrK A) {NA, Agent A, Agent B} \ 
2064  247 
\ : parts (sees lost Spy evs) > \ 
248 
\ 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

249 
\ Crypt (shrK A) {NA, Agent A, Agent B}} \ 
3465  250 
\ : set evs"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

251 
by parts_induct_tac; 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

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

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

254 

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

255 

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

257 

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

258 
goal thy 
2032  259 
"!!evs. [ evs : otway lost; A ~: lost ] \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

260 
\ ==> EX B'. ALL B. \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

261 
\ Crypt (shrK A) {NA, Agent A, Agent B} : parts (sees lost Spy evs) \ 
2048  262 
\ > B = B'"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

263 
by parts_induct_tac; 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

264 
by (Fake_parts_insert_tac 1); 
2064  265 
by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2014
diff
changeset

266 
(*OR1: creation of new Nonce. Move assertion into global context*) 
2064  267 
by (expand_case_tac "NA = ?y" 1); 
3102  268 
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

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

270 

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

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

272 
"!!evs.[ Crypt (shrK A) {NA, Agent A, Agent B}: parts(sees lost Spy evs); \ 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

273 
\ Crypt (shrK A) {NA, Agent A, Agent C}: parts(sees lost Spy evs); \ 
2048  274 
\ evs : otway lost; A ~: lost ] \ 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

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

278 

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

279 

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

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

281 
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

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

283 
goal thy 
2328  284 
"!!evs. [ A ~: lost; evs : otway lost ] \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

285 
\ ==> Crypt (shrK A) {NA, Agent A, Agent B} \ 
2328  286 
\ : parts (sees lost Spy evs) > \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

287 
\ Crypt (shrK A) {NA', NA, Agent A', Agent A} \ 
2032  288 
\ ~: parts (sees lost Spy evs)"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

289 
by parts_induct_tac; 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

290 
by (Fake_parts_insert_tac 1); 
3102  291 
by (REPEAT (blast_tac (!claset addSEs sees_Spy_partsEs 
292 
addSDs [impOfSubs parts_insert_subset_Un]) 1)); 

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

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

294 

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

295 

2053  296 
(*Crucial property: If the encrypted message appears, and A has used NA 
297 
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

298 
goal thy 
2048  299 
"!!evs. [ A ~: lost; A ~= Spy; evs : otway lost ] \ 
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} : parts (sees lost Spy evs) \ 
2048  301 
\ > 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

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

303 
\ : set evs > \ 
2048  304 
\ (EX NB. Says Server B \ 
305 
\ {NA, \ 

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

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

307 
\ Crypt (shrK B) {NB, Key K}} \ 
3465  308 
\ : set evs)"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

309 
by parts_induct_tac; 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

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

311 
(*OR1: it cannot be a new Nonce, contradiction.*) 
3102  312 
by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1); 
2064  313 
(*OR3 and OR4*) 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

314 
(*OR4*) 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

315 
by (REPEAT (Safe_step_tac 2)); 
3102  316 
by (REPEAT (blast_tac (!claset addSDs [parts_cut]) 3)); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

317 
by (fast_tac (!claset addSIs [Crypt_imp_OR1] 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

318 
addEs sees_Spy_partsEs) 2); 
2064  319 
(*OR3*) (** LEVEL 5 **) 
320 
by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1); 

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

321 
by (step_tac (!claset delrules [disjCI, impCE]) 1); 
3102  322 
by (blast_tac (!claset addSEs [MPair_parts] 
323 
addSDs [Says_imp_sees_Spy' RS parts.Inj] 

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

324 
addEs [no_nonce_OR1_OR2 RSN (2, rev_notE)] 
2048  325 
delrules [conjI] (*stop splitup into 4 subgoals*)) 2); 
3102  326 
by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] 
2048  327 
addSEs [MPair_parts] 
3102  328 
addIs [unique_NA]) 1); 
2048  329 
qed_spec_mp "NA_Crypt_imp_Server_msg"; 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

330 

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

331 

2053  332 
(*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

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

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

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

338 
\ : set evs; \ 
2053  339 
\ 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

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

341 
\ : set evs; \ 
2053  342 
\ A ~: lost; A ~= Spy; evs : otway lost ] \ 
343 
\ ==> EX NB. Says Server B \ 

2048  344 
\ {NA, \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

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

346 
\ Crypt (shrK B) {NB, Key K}} \ 
3465  347 
\ : set evs"; 
3102  348 
by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg] 
349 
addEs sees_Spy_partsEs) 1); 

2328  350 
qed "A_trusts_OR4"; 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

351 

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

352 

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

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

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

356 

1941  357 
goal thy 
2166  358 
"!!evs. [ A ~: lost; B ~: lost; evs : otway lost ] \ 
2048  359 
\ ==> Says Server B \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

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

361 
\ Crypt (shrK B) {NB, Key K}} : set evs > \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

362 
\ Says B Spy {NA, NB, Key K} ~: set evs > \ 
2048  363 
\ Key K ~: analz (sees lost Spy evs)"; 
2032  364 
by (etac otway.induct 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

365 
by analz_sees_tac; 
1964  366 
by (ALLGOALS 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

367 
(asm_simp_tac (!simpset addcongs [conj_cong] 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

368 
addsimps [analz_insert_eq, not_parts_not_analz, 
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

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

370 
setloop split_tac [expand_if]))); 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

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

372 
by (blast_tac (!claset addSDs [unique_session_keys]) 4); 
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

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

374 
by (Blast_tac 3); 
1941  375 
(*OR3*) 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

376 
by (blast_tac (!claset addSEs sees_Spy_partsEs 
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

377 
addIs [impOfSubs analz_subset_parts]) 2); 
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

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

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

380 
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

381 

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

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

383 
"!!evs. [ Says Server B \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

385 
\ Crypt (shrK B) {NB, Key K}} : set evs; \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

386 
\ Says B Spy {NA, NB, Key K} ~: set evs; \ 
2032  387 
\ A ~: lost; B ~: lost; evs : otway lost ] \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

388 
\ ==> Key K ~: analz (sees lost Spy evs)"; 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

389 
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); 
3102  390 
by (blast_tac (!claset addSEs [lemma]) 1); 
2032  391 
qed "Spy_not_see_encrypted_key"; 
392 

1945  393 

2032  394 
goal thy 
2048  395 
"!!evs. [ C ~: {A,B,Server}; \ 
396 
\ Says Server B \ 

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

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

398 
\ Crypt (shrK B) {NB, Key K}} : set evs; \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

399 
\ Says B Spy {NA, NB, Key K} ~: set evs; \ 
2032  400 
\ A ~: lost; B ~: lost; evs : otway lost ] \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

401 
\ ==> Key K ~: analz (sees lost C evs)"; 
2032  402 
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1); 
403 
by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1); 

404 
by (FIRSTGOAL (rtac Spy_not_see_encrypted_key)); 

3102  405 
by (REPEAT_FIRST (blast_tac (!claset addIs [otway_mono RS subsetD]))); 
2032  406 
qed "Agent_not_see_encrypted_key"; 
1945  407 

408 

2048  409 
(**** Authenticity properties relating to NB ****) 
410 

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

412 
know anything about X: it does NOT have to have the right form.*) 
2048  413 
goal thy 
414 
"!!evs. [ B ~: lost; evs : otway lost ] \ 

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

415 
\ ==> Crypt (shrK B) {NA, NB, Agent A, Agent B} \ 
2048  416 
\ : parts (sees lost Spy evs) > \ 
2194
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

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

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

419 
\ Crypt (shrK B) {NA, NB, Agent A, Agent B}} \ 
3465  420 
\ : set evs)"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

421 
by parts_induct_tac; 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

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

424 
bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE); 
2048  425 

426 

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

428 

429 
goal thy 

430 
"!!evs. [ evs : otway lost; B ~: lost ] \ 

2064  431 
\ ==> EX NA' A'. ALL NA A. \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

432 
\ Crypt (shrK B) {NA, NB, Agent A, Agent B} : parts(sees lost Spy evs) \ 
2048  433 
\ > NA = NA' & A = A'"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

434 
by parts_induct_tac; 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

435 
by (Fake_parts_insert_tac 1); 
2064  436 
by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
2048  437 
(*OR2: creation of new Nonce. Move assertion into global context*) 
2064  438 
by (expand_case_tac "NB = ?y" 1); 
3102  439 
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); 
2048  440 
val lemma = result(); 
441 

442 
goal thy 

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

443 
"!!evs.[ Crypt (shrK B) {NA, NB, Agent A, Agent B} \ 
2048  444 
\ : parts(sees lost Spy evs); \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

445 
\ Crypt (shrK B) {NC, NB, Agent C, Agent B} \ 
2048  446 
\ : parts(sees lost Spy evs); \ 
447 
\ evs : otway lost; B ~: lost ] \ 

448 
\ ==> NC = NA & C = A"; 

2417  449 
by (prove_unique_tac lemma 1); 
2048  450 
qed "unique_NB"; 
451 

452 

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

454 
then it originated with the Server!*) 

455 
goal thy 

456 
"!!evs. [ B ~: lost; B ~= Spy; evs : otway lost ] \ 

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

457 
\ ==> Crypt (shrK B) {NB, Key K} : parts (sees lost Spy evs) \ 
2048  458 
\ > (ALL X'. Says B Server \ 
459 
\ {NA, Agent A, Agent B, X', \ 

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

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

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

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

464 
\ Crypt (shrK B) {NB, Key K}} \ 
3465  465 
\ : set evs)"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

466 
by parts_induct_tac; 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

467 
by (Fake_parts_insert_tac 1); 
2048  468 
(*OR1: it cannot be a new Nonce, contradiction.*) 
3102  469 
by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1); 
2048  470 
(*OR4*) 
3102  471 
by (blast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2); 
2194
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

472 
(*OR3*) 
2048  473 
by (step_tac (!claset delrules [disjCI, impCE]) 1); 
3102  474 
by (blast_tac (!claset delrules [conjI] (*stop splitup*)) 3); 
475 
by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] 

476 
addSEs [MPair_parts] 

477 
addDs [unique_NB]) 2); 

478 
by (blast_tac (!claset addSEs [MPair_parts, no_nonce_OR1_OR2 RSN (2, rev_notE)] 

479 
addSDs [Says_imp_sees_Spy' RS parts.Inj] 

480 
delrules [conjI, impCE] (*stop splitup*)) 1); 

2048  481 
qed_spec_mp "NB_Crypt_imp_Server_msg"; 
482 

483 

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

485 
has sent the correct message.*) 

486 
goal thy 

487 
"!!evs. [ B ~: lost; B ~= Spy; evs : otway lost; \ 

2837
dee1c7f1f576
Trivial renamings (for consistency with CSFW papers)
paulson
parents:
2637
diff
changeset

488 
\ Says S' B {NA, X, Crypt (shrK B) {NB, Key K}} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

489 
\ : set evs; \ 
2048  490 
\ 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

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

492 
\ : set evs ] \ 
2048  493 
\ ==> Says Server B \ 
494 
\ {NA, \ 

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

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

496 
\ Crypt (shrK B) {NB, Key K}} \ 
3465  497 
\ : set evs"; 
3102  498 
by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg] 
499 
addSEs sees_Spy_partsEs) 1); 

2328  500 
qed "B_trusts_OR3"; 
2048  501 

502 

2328  503 
B_trusts_OR3 RS Spy_not_see_encrypted_key; 
2048  504 

505 

1945  506 
goal thy 
2214  507 
"!!evs. [ B ~: lost; evs : otway lost ] \ 
508 
\ ==> Says Server B \ 

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

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

510 
\ Crypt (shrK B) {NB, Key K}} : set evs > \ 
2214  511 
\ (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

512 
\ Crypt (shrK B) {NA, NB, Agent A, Agent B} } \ 
3465  513 
\ : set evs)"; 
2032  514 
by (etac otway.induct 1); 
3102  515 
by (ALLGOALS Asm_simp_tac); 
516 
by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj] 

517 
addSEs [MPair_parts, Crypt_imp_OR2]) 3); 

518 
by (ALLGOALS Blast_tac); 

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

519 
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

520 

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

521 

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

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

523 
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

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

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

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

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

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

529 
\ A ~: lost; A ~= Spy; B ~: lost; evs : otway lost ] \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

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

531 
\ Crypt (shrK B) {NA, NB, Agent A, Agent B} }\ 
3465  532 
\ : set evs"; 
3102  533 
by (blast_tac (!claset addSDs [A_trusts_OR4] 
534 
addSEs [OR3_imp_OR2]) 1); 

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

535 
qed "A_auths_B"; 