author  paulson 
Mon, 29 Sep 1997 11:47:01 +0200  
changeset 3730  6933d20f335f 
parent 3683  aafe719dff14 
child 3919  c036caebfc75 
permissions  rwrr 
2449  1 
(* Title: HOL/Auth/Recur 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1996 University of Cambridge 

5 

6 
Inductive relation "recur" for the Recursive Authentication protocol. 

7 
*) 

8 

9 
open Recur; 

10 

11 
proof_timing:=true; 

12 
HOL_quantifiers := false; 

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

13 
Pretty.setdepth 30; 
2449  14 

15 

16 
(** Possibility properties: traces that reach the end 

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

17 
ONE theorem would be more elegant and faster! 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

18 
By induction on a list of agents (no repetitions) 
2449  19 
**) 
20 

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

21 

2449  22 
(*Simplest case: Alice goes directly to the server*) 
2481  23 
goal thy 
3483
6988394a6008
Tidying; also simplified the lemma Says_Server_not
paulson
parents:
3466
diff
changeset

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

25 
\ ==> EX K NA. EX evs: recur. \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

27 
\ Agent Server} : set evs"; 
2449  28 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

29 
by (rtac (recur.Nil RS recur.RA1 RS 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

30 
(respond.One RSN (4,recur.RA3))) 2); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

31 
by possibility_tac; 
2449  32 
result(); 
33 

34 

35 
(*Case two: Alice, Bob and the server*) 

2481  36 
goal thy 
3483
6988394a6008
Tidying; also simplified the lemma Says_Server_not
paulson
parents:
3466
diff
changeset

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

38 
\ ==> EX K. EX NA. EX evs: recur. \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

40 
\ Agent Server} : set evs"; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

41 
by (cut_facts_tac [Nonce_supply2, Key_supply2] 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

42 
by (REPEAT (eresolve_tac [exE, conjE] 1)); 
2449  43 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

44 
by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

45 
(respond.One RS respond.Cons RSN (4,recur.RA3)) RS 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

46 
recur.RA4) 2); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

47 
by basic_possibility_tac; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

48 
by (DEPTH_SOLVE (eresolve_tac [asm_rl, less_not_refl2, 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

49 
less_not_refl2 RS not_sym] 1)); 
2449  50 
result(); 
51 

52 

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

53 
(*Case three: Alice, Bob, Charlie and the server 
2533  54 
TOO SLOW to run every time! 
2481  55 
goal thy 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

57 
\ ==> EX K. EX NA. EX evs: recur. \ 
3483
6988394a6008
Tidying; also simplified the lemma Says_Server_not
paulson
parents:
3466
diff
changeset

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

59 
\ Agent Server} : set evs"; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

60 
by (cut_facts_tac [Nonce_supply3, Key_supply3] 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

61 
by (REPEAT (eresolve_tac [exE, conjE] 1)); 
2449  62 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

63 
by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

64 
(respond.One RS respond.Cons RS respond.Cons RSN 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

65 
(4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

66 
(*SLOW: 70 seconds*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

67 
by basic_possibility_tac; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

68 
by (DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

70 
eresolve_tac [asm_rl, less_not_refl2, 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

71 
less_not_refl2 RS not_sym] 1)); 
2449  72 
result(); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

73 
****************) 
2449  74 

75 
(**** Inductive proofs about recur ****) 

76 

77 
(*Nobody sends themselves messages*) 

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

78 
goal thy "!!evs. evs : recur ==> ALL A X. Says A A X ~: set evs"; 
2449  79 
by (etac recur.induct 1); 
80 
by (Auto_tac()); 

81 
qed_spec_mp "not_Says_to_self"; 

82 
Addsimps [not_Says_to_self]; 

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

84 

85 

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

86 

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

87 
goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB : parts{RB}"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

88 
by (etac respond.induct 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

89 
by (ALLGOALS Simp_tac); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

90 
qed "respond_Key_in_parts"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

91 

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

92 
goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB ~: used evs"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

93 
by (etac respond.induct 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

94 
by (REPEAT (assume_tac 1)); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

95 
qed "respond_imp_not_used"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

96 

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

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

98 
"!!evs. [ Key K : parts {RB}; (PB,RB,K') : respond evs ] \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

99 
\ ==> Key K ~: used evs"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

100 
by (etac rev_mp 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

101 
by (etac respond.induct 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

102 
by (auto_tac(!claset addDs [Key_not_used, respond_imp_not_used], 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

103 
!simpset)); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

104 
qed_spec_mp "Key_in_parts_respond"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

105 

2449  106 
(*Simple inductive reasoning about responses*) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

107 
goal thy "!!evs. (PA,RB,KAB) : respond evs ==> RB : responses evs"; 
2449  108 
by (etac respond.induct 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

109 
by (REPEAT (ares_tac (respond_imp_not_used::responses.intrs) 1)); 
2449  110 
qed "respond_imp_responses"; 
111 

112 

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

114 

3683  115 
val RA2_analz_spies = Says_imp_spies RS analz.Inj > standard; 
2449  116 

3465  117 
goal thy "!!evs. Says C' B {Crypt K X, X', RA} : set evs \ 
3683  118 
\ ==> RA : analz (spies evs)"; 
119 
by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1); 

120 
qed "RA4_analz_spies"; 

2449  121 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

122 
(*RA2_analz... and RA4_analz... let us treat those cases using the same 
2449  123 
argument as for the Fake case. This is possible for most, but not all, 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

124 
proofs: Fake does not invent new nonces (as in RA2), and of course Fake 
2449  125 
messages originate from the Spy. *) 
126 

3683  127 
bind_thm ("RA2_parts_spies", 
128 
RA2_analz_spies RS (impOfSubs analz_subset_parts)); 

129 
bind_thm ("RA4_parts_spies", 

130 
RA4_analz_spies RS (impOfSubs analz_subset_parts)); 

2449  131 

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

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

134 
etac recur.induct i THEN 
3683  135 
forward_tac [RA2_parts_spies] (i+3) THEN 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

136 
etac subst (i+3) (*RA2: DELETE needless definition of PA!*) THEN 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

137 
forward_tac [respond_imp_responses] (i+4) THEN 
3683  138 
forward_tac [RA4_parts_spies] (i+5) THEN 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

139 
prove_simple_subgoals_tac i; 
2449  140 

141 

3683  142 
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY 
2449  143 
sends messages containing X! **) 
144 

145 

3683  146 
(** Spy never sees another agent's shared key! (unless it's bad at start) **) 
2449  147 

148 
goal thy 

3683  149 
"!!evs. evs : recur ==> (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

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

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

152 
by (ALLGOALS 
3683  153 
(asm_simp_tac (!simpset addsimps [parts_insert2, parts_insert_spies]))); 
2550
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

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

155 
by (blast_tac (!claset addDs [Key_in_parts_respond]) 2); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

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

157 
by (blast_tac (!claset addSEs partsEs addDs [parts_cut]) 1); 
2449  158 
qed "Spy_see_shrK"; 
159 
Addsimps [Spy_see_shrK]; 

160 

161 
goal thy 

3683  162 
"!!evs. evs : recur ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; 
2449  163 
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); 
164 
qed "Spy_analz_shrK"; 

165 
Addsimps [Spy_analz_shrK]; 

166 

3683  167 
goal thy "!!A. [ Key (shrK A) : parts (spies evs); evs : recur ] ==> A:bad"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

168 
by (blast_tac (!claset addDs [Spy_see_shrK]) 1); 
2449  169 
qed "Spy_see_shrK_D"; 
170 

171 
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); 

172 
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; 

173 

174 

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

175 

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

176 
(** Nobody can have used nonexistent keys! **) 
2449  177 

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

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

179 
"!!evs. [ K : keysFor (parts {RB}); (PB,RB,K') : respond evs ] \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

180 
\ ==> K : range shrK"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

181 
by (etac rev_mp 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

182 
by (etac (respond_imp_responses RS responses.induct) 1); 
2449  183 
by (Auto_tac()); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

184 
qed_spec_mp "Key_in_keysFor_parts"; 
2449  185 

186 

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

187 
goal thy "!!evs. evs : recur ==> \ 
3683  188 
\ 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

189 
by (parts_induct_tac 1); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

190 
(*RA3*) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

191 
by (best_tac (!claset addDs [Key_in_keysFor_parts] 
3683  192 
addss (!simpset addsimps [parts_insert_spies])) 2); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

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

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

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

197 
impOfSubs (parts_insert_subset_Un RS keysFor_mono)] 
3207  198 
addss (!simpset)) 1); 
2449  199 
qed_spec_mp "new_keys_not_used"; 
200 

201 

202 
bind_thm ("new_keys_not_analzd", 

203 
[analz_subset_parts RS keysFor_mono, 

204 
new_keys_not_used] MRS contra_subsetD); 

205 

206 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 

207 

208 

209 

210 
(*** Proofs involving analz ***) 

211 

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

212 
(*For proofs involving analz.*) 
3683  213 
val analz_spies_tac = 
2485
c4368c967c56
Simplification of some proofs, especially by eliminating
paulson
parents:
2481
diff
changeset

214 
etac subst 4 (*RA2: DELETE needless definition of PA!*) THEN 
3683  215 
dtac RA2_analz_spies 4 THEN 
2449  216 
forward_tac [respond_imp_responses] 5 THEN 
3683  217 
dtac RA4_analz_spies 6; 
2449  218 

219 

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

221 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

222 
(*Version for "responses" relation. Handles case RA3 in the theorem below. 
3683  223 
Note that it holds for *any* set H (not just "spies evs") 
2449  224 
satisfying the inductive hypothesis.*) 
225 
goal thy 

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

226 
"!!evs. [ RB : responses evs; \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

227 
\ ALL K KK. KK <= Compl (range shrK) > \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

228 
\ (Key K : analz (Key``KK Un H)) = \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

229 
\ (K : KK  Key K : analz H) ] \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

230 
\ ==> ALL K KK. KK <= Compl (range shrK) > \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

231 
\ (Key K : analz (insert RB (Key``KK Un H))) = \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

232 
\ (K : KK  Key K : analz (insert RB H))"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

233 
by (etac responses.induct 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

234 
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

235 
qed "resp_analz_image_freshK_lemma"; 
2449  236 

237 
(*Version for the protocol. Proof is almost trivial, thanks to the lemma.*) 

238 
goal thy 

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

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

240 
\ ALL K KK. KK <= Compl (range shrK) > \ 
3683  241 
\ (Key K : analz (Key``KK Un (spies evs))) = \ 
242 
\ (K : KK  Key K : analz (spies evs))"; 

2449  243 
by (etac recur.induct 1); 
3683  244 
by analz_spies_tac; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

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

247 
by (ALLGOALS 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

248 
(asm_simp_tac 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

249 
(analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma]))); 
2449  250 
(*Base*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

251 
by (Blast_tac 1); 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

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

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

254 
val raw_analz_image_freshK = result(); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

255 
qed_spec_mp "analz_image_freshK"; 
2449  256 

257 

3683  258 
(*Instance of the lemma with H replaced by (spies evs): 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

259 
[ RB : responses evs; evs : recur; ] 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

260 
==> KK <= Compl (range shrK) > 
3683  261 
Key K : analz (insert RB (Key``KK Un spies evs)) = 
262 
(K : KK  Key K : analz (insert RB (spies evs))) 

2449  263 
*) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

264 
bind_thm ("resp_analz_image_freshK", 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

265 
raw_analz_image_freshK RSN 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

266 
(2, resp_analz_image_freshK_lemma) RS spec RS spec); 
2449  267 

268 
goal thy 

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

269 
"!!evs. [ evs : recur; KAB ~: range shrK ] ==> \ 
3683  270 
\ Key K : analz (insert (Key KAB) (spies evs)) = \ 
271 
\ (K = KAB  Key K : analz (spies evs))"; 

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

272 
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:
2485
diff
changeset

273 
qed "analz_insert_freshK"; 
2449  274 

275 

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

276 
(*Everything that's hashed is already in past traffic. *) 
3683  277 
goal thy "!!evs. [ Hash {Key(shrK A), X} : parts (spies evs); \ 
278 
\ evs : recur; A ~: bad ] \ 

279 
\ ==> X : parts (spies evs)"; 

2550
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

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

281 
by (parts_induct_tac 1); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

282 
(*RA3 requires a further induction*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

283 
by (etac responses.induct 2); 
2449  284 
by (ALLGOALS Asm_simp_tac); 
285 
(*Fake*) 

3683  286 
by (simp_tac (!simpset addsimps [parts_insert_spies]) 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

287 
by (Fake_parts_insert_tac 1); 
2550
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

288 
qed "Hash_imp_body"; 
2449  289 

290 

291 
(** The Nonce NA uniquely identifies A's message. 

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

292 
This theorem applies to steps RA1 and RA2! 
2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

293 

9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

294 
Unicity is not used in other proofs but is desirable in its own right. 
2449  295 
**) 
296 

297 
goal thy 

3683  298 
"!!evs. [ evs : recur; A ~: bad ] \ 
2560  299 
\ ==> EX B' P'. ALL B P. \ 
3683  300 
\ Hash {Key(shrK A), Agent A, B, NA, P} : parts (spies evs) \ 
2560  301 
\ > B=B' & P=P'"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

304 
by (etac responses.induct 3); 
2485
c4368c967c56
Simplification of some proofs, especially by eliminating
paulson
parents:
2481
diff
changeset

305 
by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib]))); 
3730  306 
by (clarify_tac (!claset addSEs partsEs) 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

307 
(*RA1,2: creation of new Nonce. Move assertion into global context*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

308 
by (ALLGOALS (expand_case_tac "NA = ?y")); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

309 
by (REPEAT_FIRST (ares_tac [exI])); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

310 
by (REPEAT (blast_tac (!claset addSDs [Hash_imp_body] 
3683  311 
addSEs spies_partsEs) 1)); 
2449  312 
val lemma = result(); 
313 

2481  314 
goalw thy [HPair_def] 
3683  315 
"!!A.[ Hash[Key(shrK A)] {Agent A, B,NA,P} : parts(spies evs); \ 
316 
\ Hash[Key(shrK A)] {Agent A, B',NA,P'} : parts(spies evs); \ 

317 
\ evs : recur; A ~: bad ] \ 

3483
6988394a6008
Tidying; also simplified the lemma Says_Server_not
paulson
parents:
3466
diff
changeset

318 
\ ==> B=B' & P=P'"; 
2481  319 
by (REPEAT (eresolve_tac partsEs 1)); 
2449  320 
by (prove_unique_tac lemma 1); 
321 
qed "unique_NA"; 

322 

323 

324 
(*** Lemmas concerning the Server's response 

325 
(relations "respond" and "responses") 

326 
***) 

327 

328 
goal thy 

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

329 
"!!evs. [ RB : responses evs; evs : recur ] \ 
3683  330 
\ ==> (Key (shrK B) : analz (insert RB (spies evs))) = (B:bad)"; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

331 
by (etac responses.induct 1); 
2449  332 
by (ALLGOALS 
333 
(asm_simp_tac 

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

334 
(analz_image_freshK_ss addsimps [Spy_analz_shrK, 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

335 
resp_analz_image_freshK]))); 
2449  336 
qed "shrK_in_analz_respond"; 
337 
Addsimps [shrK_in_analz_respond]; 

338 

339 

340 
goal thy 

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

341 
"!!evs. [ RB : responses evs; \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

342 
\ ALL K KK. KK <= Compl (range shrK) > \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

343 
\ (Key K : analz (Key``KK Un H)) = \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

344 
\ (K : KK  Key K : analz H) ] \ 
3483
6988394a6008
Tidying; also simplified the lemma Says_Server_not
paulson
parents:
3466
diff
changeset

345 
\ ==> (Key K : analz (insert RB H)) > \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

346 
\ (Key K : parts{RB}  Key K : analz H)"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

347 
by (etac responses.induct 1); 
2449  348 
by (ALLGOALS 
349 
(asm_simp_tac 

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

350 
(analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma]))); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

351 
(*Simplification using two distinct treatments of "image"*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

352 
by (simp_tac (!simpset addsimps [parts_insert2]) 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

353 
by (blast_tac (!claset delrules [allE]) 1); 
2449  354 
qed "resp_analz_insert_lemma"; 
355 

356 
bind_thm ("resp_analz_insert", 

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

357 
raw_analz_image_freshK RSN 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

358 
(2, resp_analz_insert_lemma) RSN(2, rev_mp)); 
2449  359 

360 

361 
(*The Server does not send such messages. This theorem lets us avoid 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

362 
assuming B~=Server in RA4.*) 
2449  363 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

364 
"!!evs. evs : recur \ 
3483
6988394a6008
Tidying; also simplified the lemma Says_Server_not
paulson
parents:
3466
diff
changeset

365 
\ ==> ALL C X Y. Says Server C {X, Agent Server, Y} ~: set evs"; 
2449  366 
by (etac recur.induct 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

367 
by (etac (respond.induct) 5); 
2449  368 
by (Auto_tac()); 
369 
qed_spec_mp "Says_Server_not"; 

370 
AddSEs [Says_Server_not RSN (2,rev_notE)]; 

371 

372 

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

373 
(*The last key returned by respond indeed appears in a certificate*) 
2449  374 
goal thy 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

375 
"!!K. (Hash[Key(shrK A)] {Agent A, B, NA, P}, RA, K) : respond evs \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

376 
\ ==> Crypt (shrK A) {Key K, B, NA} : parts {RA}"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

377 
by (etac respond.elim 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

378 
by (ALLGOALS Asm_full_simp_tac); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

379 
qed "respond_certificate"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

380 

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

381 

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

382 
goal thy 
2560  383 
"!!K'. (PB,RB,KXY) : respond evs \ 
384 
\ ==> EX A' B'. ALL A B N. \ 

2449  385 
\ Crypt (shrK A) {Key K, Agent B, N} : parts {RB} \ 
386 
\ > (A'=A & B'=B)  (A'=B & B'=A)"; 

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

387 
by (etac respond.induct 1); 
2449  388 
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [all_conj_distrib]))); 
389 
(*Base case*) 

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

390 
by (Blast_tac 1); 
3730  391 
by Safe_tac; 
2550
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

392 
by (expand_case_tac "K = KBC" 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

394 
by (blast_tac (!claset addSIs [exI] 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

396 
addDs [Key_in_parts_respond]) 1); 
2550
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

397 
by (expand_case_tac "K = KAB" 1); 
2449  398 
by (REPEAT (ares_tac [exI] 2)); 
399 
by (ex_strip_tac 1); 

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

400 
by (dtac respond_certificate 1); 
2449  401 
by (Fast_tac 1); 
402 
val lemma = result(); 

403 

404 
goal thy 

2560  405 
"!!RB. [ Crypt (shrK A) {Key K, Agent B, N} : parts {RB}; \ 
2449  406 
\ Crypt (shrK A') {Key K, Agent B', N'} : parts {RB}; \ 
2560  407 
\ (PB,RB,KXY) : respond evs ] \ 
2449  408 
\ ==> (A'=A & B'=B)  (A'=B & B'=A)"; 
2560  409 
by (prove_unique_tac lemma 1); 
2449  410 
qed "unique_session_keys"; 
411 

412 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

413 
(** Crucial secrecy property: Spy does not see the keys sent in msg RA3 
2449  414 
Does not in itself guarantee security: an attack could violate 
415 
the premises, e.g. by having A=Spy **) 

416 

417 
goal thy 

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

418 
"!!evs. [ (PB,RB,KAB) : respond evs; evs : recur ] \ 
3683  419 
\ ==> ALL A A' N. A ~: bad & A' ~: bad > \ 
2449  420 
\ Crypt (shrK A) {Key K, Agent A', N} : parts{RB} > \ 
3683  421 
\ Key K ~: analz (insert RB (spies evs))"; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

422 
by (etac respond.induct 1); 
2449  423 
by (forward_tac [respond_imp_responses] 2); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

424 
by (forward_tac [respond_imp_not_used] 2); 
3681  425 
by (ALLGOALS (*12 seconds*) 
2449  426 
(asm_simp_tac 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

427 
(analz_image_freshK_ss addsimps 
2533  428 
[shrK_in_analz_respond, resp_analz_image_freshK, parts_insert2]))); 
3681  429 
by (ALLGOALS (simp_tac (!simpset addsimps [ex_disj_distrib]))); 
430 
(** LEVEL 5 **) 

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

431 
by (blast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1); 
3730  432 
by (safe_tac (!claset addSEs [MPair_parts])); 
3681  433 
by (REPEAT (blast_tac (!claset addSDs [respond_certificate] 
434 
addDs [resp_analz_insert] 

435 
addIs [impOfSubs analz_subset_parts]) 4)); 

436 
by (Blast_tac 3); 

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

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

438 
addDs [Key_in_parts_respond]) 2); 
3683  439 
(*by unicity, either B=Aa or B=A', a contradiction since B: bad*) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

440 
by (dtac unique_session_keys 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

441 
by (etac respond_certificate 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

443 
by (Blast_tac 1); 
2533  444 
qed_spec_mp "respond_Spy_not_see_session_key"; 
2449  445 

446 

447 
goal thy 

3683  448 
"!!evs. [ Crypt (shrK A) {Key K, Agent A', N} : parts (spies evs); \ 
3730  449 
\ A ~: bad; A' ~: bad; evs : recur ] \ 
3683  450 
\ ==> Key K ~: analz (spies evs)"; 
2550
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

451 
by (etac rev_mp 1); 
2449  452 
by (etac recur.induct 1); 
3683  453 
by analz_spies_tac; 
2449  454 
by (ALLGOALS 
455 
(asm_simp_tac 

3730  456 
(!simpset addsimps [analz_insert_eq, parts_insert_spies, 
457 
analz_insert_freshK] 

2449  458 
setloop split_tac [expand_if]))); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

459 
(*RA4*) 
2533  460 
by (spy_analz_tac 5); 
461 
(*RA2*) 

462 
by (spy_analz_tac 3); 

2449  463 
(*Fake*) 
2533  464 
by (spy_analz_tac 2); 
465 
(*Base*) 

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

466 
by (Blast_tac 1); 
2533  467 
(*RA3 remains*) 
3730  468 
by (safe_tac (!claset delrules [impCE])); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

469 
(*RA3, case 2: K is an old key*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

471 
addSEs partsEs 
3730  472 
addDs [Key_in_parts_respond]) 2); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

473 
(*RA3, case 1: use lemma previously proved by induction*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

474 
by (blast_tac (!claset addSEs [respond_Spy_not_see_session_key RSN 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

475 
(2,rev_notE)]) 1); 
2550
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

476 
qed "Spy_not_see_session_key"; 
2449  477 

478 

479 
(**** Authenticity properties for Agents ****) 

480 

2481  481 
(*The response never contains Hashes*) 
482 
goal thy 

2550
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

483 
"!!evs. [ Hash {Key (shrK B), M} : parts (insert RB H); \ 
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

484 
\ (PB,RB,K) : respond evs ] \ 
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

485 
\ ==> Hash {Key (shrK B), M} : parts H"; 
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

486 
by (etac rev_mp 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

487 
by (etac (respond_imp_responses RS responses.induct) 1); 
2481  488 
by (Auto_tac()); 
2550
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

489 
qed "Hash_in_parts_respond"; 
2481  490 

2533  491 
(*Only RA1 or RA2 can have caused such a part of a message to appear. 
492 
This result is of no use to B, who cannot verify the Hash. Moreover, 

493 
it can say nothing about how recent A's message is. It might later be 

494 
used to prove B's presence to A at the run's conclusion.*) 

2481  495 
goalw thy [HPair_def] 
3683  496 
"!!evs. [ Hash {Key(shrK A), Agent A, Agent B, NA, P} : parts(spies evs); \ 
497 
\ A ~: bad; evs : recur ] \ 

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

498 
\ ==> Says A B (Hash[Key(shrK A)] {Agent A, Agent B, NA, P}) : set evs"; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

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

501 
by (Fake_parts_insert_tac 1); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

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

503 
by (blast_tac (!claset addSDs [Hash_in_parts_respond]) 1); 
2449  504 
qed_spec_mp "Hash_auth_sender"; 
505 

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

506 
(** These two results subsume (for all agents) the guarantees proved 
2449  507 
separately for A and B in the OtwayRees protocol. 
508 
**) 

509 

510 

2533  511 
(*Certificates can only originate with the Server.*) 
2449  512 
goal thy 
3683  513 
"!!evs. [ Crypt (shrK A) Y : parts (spies evs); \ 
514 
\ A ~: bad; A ~= Spy; evs : recur ] \ 

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

515 
\ ==> EX C RC. Says Server C RC : set evs & \ 
2550
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

516 
\ Crypt (shrK A) Y : parts {RC}"; 
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

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

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

519 
by (Fake_parts_insert_tac 1); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

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

521 
by (Blast_tac 4); 
2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

522 
(*RA3*) 
3683  523 
by (full_simp_tac (!simpset addsimps [parts_insert_spies]) 3 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

524 
THEN Blast_tac 3); 
2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

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

526 
by (Blast_tac 1); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

527 
(*RA2: it cannot be a new Nonce, contradiction.*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

528 
by (Blast_tac 1); 
2550
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

529 
qed "Cert_imp_Server_msg"; 