author  nipkow 
Thu, 26 Jun 1997 13:20:50 +0200  
changeset 3465  e85c24717cad 
parent 3451  d10f100676d8 
child 3466  30791e5a69c4 
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 
2449  24 
"!!A. A ~= Server \ 
25 
\ ==> EX K NA. EX evs: recur lost. \ 

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}, \ 
2550
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

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

30 
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

31 
(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

32 
by possibility_tac; 
2449  33 
result(); 
34 

35 

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

2481  37 
goal thy 
2449  38 
"!!A B. [ A ~= B; A ~= Server; B ~= Server ] \ 
2550
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

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

40 
\ Says B A {Crypt (shrK A) {Key K, Agent B, Nonce NA}, \ 
2550
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

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

43 
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

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

46 
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

47 
(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

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

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

50 
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

51 
less_not_refl2 RS not_sym] 1)); 
2449  52 
result(); 
53 

54 

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

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

58 
"!!A B. [ A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server ] \ 
2550
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

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

60 
\ Says B A {Crypt (shrK A) {Key K, Agent B, Nonce NA}, \ 
2550
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

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

63 
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

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

66 
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

67 
(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

68 
(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

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

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

71 
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

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

73 
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

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

76 
****************) 
2449  77 

78 
(**** Inductive proofs about recur ****) 

79 

80 
(*Monotonicity*) 

81 
goal thy "!!evs. lost' <= lost ==> recur lost' <= recur lost"; 

82 
by (rtac subsetI 1); 

83 
by (etac recur.induct 1); 

84 
by (REPEAT_FIRST 

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

85 
(blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono) 
2449  86 
:: recur.intrs)))); 
87 
qed "recur_mono"; 

88 

89 
(*Nobody sends themselves messages*) 

3465  90 
goal thy "!!evs. evs : recur lost ==> ALL A X. Says A A X ~: set evs"; 
2449  91 
by (etac recur.induct 1); 
92 
by (Auto_tac()); 

93 
qed_spec_mp "not_Says_to_self"; 

94 
Addsimps [not_Says_to_self]; 

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

96 

97 

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

98 

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

99 
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

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

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

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

103 

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

104 
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

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

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

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

108 

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

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

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

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

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

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

114 
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

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

116 
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

117 

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

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

121 
by (REPEAT (ares_tac (respond_imp_not_used::responses.intrs) 1)); 
2449  122 
qed "respond_imp_responses"; 
123 

124 

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

126 

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

127 
val RA2_analz_sees_Spy = Says_imp_sees_Spy RS analz.Inj > standard; 
2449  128 

3465  129 
goal thy "!!evs. Says C' B {Crypt K X, X', RA} : set evs \ 
2449  130 
\ ==> RA : analz (sees lost Spy evs)"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

131 
by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

132 
qed "RA4_analz_sees_Spy"; 
2449  133 

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

134 
(*RA2_analz... and RA4_analz... let us treat those cases using the same 
2449  135 
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

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

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

139 
bind_thm ("RA2_parts_sees_Spy", 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

140 
RA2_analz_sees_Spy RS (impOfSubs analz_subset_parts)); 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

141 
bind_thm ("RA4_parts_sees_Spy", 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

142 
RA4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); 
2449  143 

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

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

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

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

147 
val parts_induct_tac = 
2449  148 
let val tac = forw_inst_tac [("lost","lost")] 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

149 
in etac recur.induct 1 THEN 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

150 
tac RA2_parts_sees_Spy 4 THEN 
2485
c4368c967c56
Simplification of some proofs, especially by eliminating
paulson
parents:
2481
diff
changeset

151 
etac subst 4 (*RA2: DELETE needless definition of PA!*) THEN 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

152 
forward_tac [respond_imp_responses] 5 THEN 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

153 
tac RA4_parts_sees_Spy 6 THEN 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

154 
prove_simple_subgoals_tac 1 
2449  155 
end; 
156 

157 

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

159 
sends messages containing X! **) 

160 

161 

162 
(** Spy never sees another agent's longterm key (unless initially lost) **) 

163 

164 
goal thy 

165 
"!!evs. evs : recur lost \ 

166 
\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; 

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

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

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

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

170 
(asm_simp_tac (!simpset addsimps [parts_insert2, parts_insert_sees]))); 
2550
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

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

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

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

174 
by (blast_tac (!claset addSEs partsEs addDs [parts_cut]) 1); 
2449  175 
qed "Spy_see_shrK"; 
176 
Addsimps [Spy_see_shrK]; 

177 

178 
goal thy 

179 
"!!evs. evs : recur lost \ 

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

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

182 
qed "Spy_analz_shrK"; 

183 
Addsimps [Spy_analz_shrK]; 

184 

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

186 
\ evs : recur lost ] ==> A:lost"; 

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

187 
by (blast_tac (!claset addDs [Spy_see_shrK]) 1); 
2449  188 
qed "Spy_see_shrK_D"; 
189 

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

191 
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; 

192 

193 

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

194 

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

195 
(** Nobody can have used nonexistent keys! **) 
2449  196 

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

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

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

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

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

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

203 
qed_spec_mp "Key_in_keysFor_parts"; 
2449  204 

205 

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

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

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

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

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

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

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

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

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

215 
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

216 
impOfSubs (parts_insert_subset_Un RS keysFor_mono)] 
3207  217 
addss (!simpset)) 1); 
2449  218 
qed_spec_mp "new_keys_not_used"; 
219 

220 

221 
bind_thm ("new_keys_not_analzd", 

222 
[analz_subset_parts RS keysFor_mono, 

223 
new_keys_not_used] MRS contra_subsetD); 

224 

225 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 

226 

227 

228 

229 
(*** Proofs involving analz ***) 

230 

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

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

232 
val analz_sees_tac = 
2485
c4368c967c56
Simplification of some proofs, especially by eliminating
paulson
parents:
2481
diff
changeset

233 
etac subst 4 (*RA2: DELETE needless definition of PA!*) THEN 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

234 
dres_inst_tac [("lost","lost")] RA2_analz_sees_Spy 4 THEN 
2449  235 
forward_tac [respond_imp_responses] 5 THEN 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

236 
dres_inst_tac [("lost","lost")] RA4_analz_sees_Spy 6; 
2449  237 

238 

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

240 

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

241 
(*Version for "responses" relation. Handles case RA3 in the theorem below. 
2449  242 
Note that it holds for *any* set H (not just "sees lost Spy evs") 
243 
satisfying the inductive hypothesis.*) 

244 
goal thy 

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

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

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

247 
\ (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

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

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

250 
\ (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

251 
\ (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

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

253 
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

254 
qed "resp_analz_image_freshK_lemma"; 
2449  255 

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

257 
goal thy 

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

258 
"!!evs. evs : recur lost ==> \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

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

261 
\ (K : KK  Key K : analz (sees lost Spy evs))"; 
2449  262 
by (etac recur.induct 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

264 
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

265 
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

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

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

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

270 
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

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

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

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

274 
qed_spec_mp "analz_image_freshK"; 
2449  275 

276 

277 
(*Instance of the lemma with H replaced by (sees lost Spy evs): 

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

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

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

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

281 
(K : KK  Key K : analz (insert RB (sees lost Spy evs))) 
2449  282 
*) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

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

285 
(2, resp_analz_image_freshK_lemma) RS spec RS spec); 
2449  286 

287 
goal thy 

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

288 
"!!evs. [ evs : recur lost; KAB ~: range shrK ] ==> \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

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

291 
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

292 
qed "analz_insert_freshK"; 
2449  293 

294 

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

295 
(*Everything that's hashed is already in past traffic. *) 
2550
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

296 
goal thy "!!evs. [ Hash {Key(shrK A), X} : parts (sees lost Spy evs); \ 
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

297 
\ evs : recur lost; A ~: lost ] \ 
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

298 
\ ==> X : parts (sees lost Spy evs)"; 
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

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

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

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

302 
by (etac responses.induct 2); 
2449  303 
by (ALLGOALS Asm_simp_tac); 
304 
(*Fake*) 

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

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

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

307 
qed "Hash_imp_body"; 
2449  308 

309 

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

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

312 

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

313 
Unicity is not used in other proofs but is desirable in its own right. 
2449  314 
**) 
315 

316 
goal thy 

2560  317 
"!!evs. [ evs : recur lost; A ~: lost ] \ 
318 
\ ==> EX B' P'. ALL B P. \ 

319 
\ Hash {Key(shrK A), Agent A, B, NA, P} : parts (sees lost Spy evs) \ 

320 
\ > B=B' & P=P'"; 

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

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

322 
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

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

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

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

327 
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

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

329 
by (REPEAT (blast_tac (!claset addSDs [Hash_imp_body] 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

330 
addSEs sees_Spy_partsEs) 1)); 
2449  331 
val lemma = result(); 
332 

2481  333 
goalw thy [HPair_def] 
2560  334 
"!!evs.[ Hash[Key(shrK A)] {Agent A,B,NA,P} : parts (sees lost Spy evs); \ 
335 
\ Hash[Key(shrK A)] {Agent A,B',NA,P'} : parts (sees lost Spy evs);\ 

336 
\ evs : recur lost; A ~: lost ] \ 

2449  337 
\ ==> B=B' & P=P'"; 
2481  338 
by (REPEAT (eresolve_tac partsEs 1)); 
2449  339 
by (prove_unique_tac lemma 1); 
340 
qed "unique_NA"; 

341 

342 

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

344 
(relations "respond" and "responses") 

345 
***) 

346 

347 
goal thy 

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

348 
"!!evs. [ RB : responses evs; evs : recur lost ] \ 
2449  349 
\ ==> (Key (shrK B) : analz (insert RB (sees lost Spy evs))) = (B:lost)"; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

350 
by (etac responses.induct 1); 
2449  351 
by (ALLGOALS 
352 
(asm_simp_tac 

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

353 
(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

354 
resp_analz_image_freshK]))); 
2449  355 
qed "shrK_in_analz_respond"; 
356 
Addsimps [shrK_in_analz_respond]; 

357 

358 

359 
goal thy 

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

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

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

362 
\ (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

363 
\ (K : KK  Key K : analz H) ] \ 
2449  364 
\ ==> (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

365 
\ (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

366 
by (etac responses.induct 1); 
2449  367 
by (ALLGOALS 
368 
(asm_simp_tac 

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

369 
(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

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

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

372 
by (blast_tac (!claset delrules [allE]) 1); 
2449  373 
qed "resp_analz_insert_lemma"; 
374 

375 
bind_thm ("resp_analz_insert", 

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

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

377 
(2, resp_analz_insert_lemma) RSN(2, rev_mp)); 
2449  378 

379 

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

381 
assuming B~=Server in RA4.*) 
2449  382 
goal thy 
383 
"!!evs. evs : recur lost \ 

384 
\ ==> ALL C X Y P. Says Server C {X, Agent Server, Agent C, Y, P} \ 

3465  385 
\ ~: set evs"; 
2449  386 
by (etac recur.induct 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

387 
by (etac (respond.induct) 5); 
2449  388 
by (Auto_tac()); 
389 
qed_spec_mp "Says_Server_not"; 

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

391 

392 

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

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

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

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

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

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

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

400 

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

401 

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

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

2449  405 
\ Crypt (shrK A) {Key K, Agent B, N} : parts {RB} \ 
406 
\ > (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

407 
by (etac respond.induct 1); 
2449  408 
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [all_conj_distrib]))); 
409 
(*Base case*) 

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

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

412 
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

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

414 
by (blast_tac (!claset addSIs [exI] 
2449  415 
addSEs partsEs 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

417 
by (expand_case_tac "K = KAB" 1); 
2449  418 
by (REPEAT (ares_tac [exI] 2)); 
419 
by (ex_strip_tac 1); 

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

420 
by (dtac respond_certificate 1); 
2449  421 
by (Fast_tac 1); 
422 
val lemma = result(); 

423 

424 
goal thy 

2560  425 
"!!RB. [ Crypt (shrK A) {Key K, Agent B, N} : parts {RB}; \ 
2449  426 
\ Crypt (shrK A') {Key K, Agent B', N'} : parts {RB}; \ 
2560  427 
\ (PB,RB,KXY) : respond evs ] \ 
2449  428 
\ ==> (A'=A & B'=B)  (A'=B & B'=A)"; 
2560  429 
by (prove_unique_tac lemma 1); 
2449  430 
qed "unique_session_keys"; 
431 

432 

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

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

436 

437 
goal thy 

2533  438 
"!!evs. [ (PB,RB,KAB) : respond evs; evs : recur lost ] \ 
439 
\ ==> ALL A A' N. A ~: lost & A' ~: lost > \ 

2449  440 
\ Crypt (shrK A) {Key K, Agent A', N} : parts{RB} > \ 
441 
\ Key K ~: analz (insert RB (sees lost Spy evs))"; 

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

442 
by (etac respond.induct 1); 
2449  443 
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

444 
by (forward_tac [respond_imp_not_used] 2); 
2533  445 
by (ALLGOALS (*23 seconds*) 
2449  446 
(asm_simp_tac 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

447 
(analz_image_freshK_ss addsimps 
2533  448 
[shrK_in_analz_respond, resp_analz_image_freshK, parts_insert2]))); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

449 
by (ALLGOALS Simp_tac); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

450 
by (blast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1); 
2449  451 
by (step_tac (!claset addSEs [MPair_parts]) 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

453 
by (blast_tac (!claset addSDs [resp_analz_insert, Key_in_parts_respond] 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

454 
addDs [impOfSubs analz_subset_parts]) 4); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

455 
by (blast_tac (!claset addSDs [respond_certificate]) 3); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

457 
addDs [Key_in_parts_respond]) 2); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

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

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

461 
by (Blast_tac 1); 
2533  462 
qed_spec_mp "respond_Spy_not_see_session_key"; 
2449  463 

464 

465 
goal thy 

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

466 
"!!evs. [ Crypt (shrK A) {Key K, Agent A', N} \ 
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

467 
\ : parts (sees lost Spy evs); \ 
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

468 
\ A ~: lost; A' ~: lost; evs : recur lost ] \ 
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

469 
\ ==> Key K ~: analz (sees lost Spy evs)"; 
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

470 
by (etac rev_mp 1); 
2449  471 
by (etac recur.induct 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

472 
by analz_sees_tac; 
2449  473 
by (ALLGOALS 
474 
(asm_simp_tac 

2533  475 
(!simpset addsimps [parts_insert_sees, analz_insert_freshK] 
2449  476 
setloop split_tac [expand_if]))); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

477 
(*RA4*) 
2533  478 
by (spy_analz_tac 5); 
479 
(*RA2*) 

480 
by (spy_analz_tac 3); 

2449  481 
(*Fake*) 
2533  482 
by (spy_analz_tac 2); 
483 
(*Base*) 

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

484 
by (Blast_tac 1); 
2533  485 
(*RA3 remains*) 
2449  486 
by (step_tac (!claset delrules [impCE]) 1); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

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

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

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

490 
addDs [Key_in_parts_respond]) 2); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

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

492 
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

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

494 
qed "Spy_not_see_session_key"; 
2449  495 

496 

497 
goal thy 

2533  498 
"!!evs. [ Crypt (shrK A) {Key K, Agent A', N} \ 
499 
\ : parts(sees lost Spy evs); \ 

500 
\ C ~: {A,A',Server}; \ 

501 
\ A ~: lost; A' ~: lost; evs : recur lost ] \ 

2449  502 
\ ==> Key K ~: analz (sees lost C evs)"; 
503 
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1); 

504 
by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1); 

2533  505 
by (FIRSTGOAL (rtac Spy_not_see_session_key)); 
506 
by (REPEAT_FIRST 

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

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

508 
(!claset addIs (map impOfSubs [recur_mono, parts_mono, sees_mono])))); 
2533  509 
qed "Agent_not_see_session_key"; 
2449  510 

511 

512 
(**** Authenticity properties for Agents ****) 

513 

2481  514 
(*The response never contains Hashes*) 
515 
goal thy 

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

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

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

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

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

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

522 
qed "Hash_in_parts_respond"; 
2481  523 

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

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

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

2481  528 
goalw thy [HPair_def] 
2449  529 
"!!evs. [ Hash {Key(shrK A), Agent A, Agent B, NA, P} \ 
530 
\ : parts (sees lost Spy evs); \ 

531 
\ A ~: lost; evs : recur lost ] \ 

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

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

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

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

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

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

538 
by (blast_tac (!claset addSDs [Hash_in_parts_respond]) 1); 
2449  539 
qed_spec_mp "Hash_auth_sender"; 
540 

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

541 
(** These two results subsume (for all agents) the guarantees proved 
2449  542 
separately for A and B in the OtwayRees protocol. 
543 
**) 

544 

545 

2533  546 
(*Certificates can only originate with the Server.*) 
2449  547 
goal thy 
2550
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

548 
"!!evs. [ Crypt (shrK A) Y : parts (sees lost Spy evs); \ 
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

549 
\ A ~: lost; A ~= Spy; evs : recur lost ] \ 
3465  550 
\ ==> 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

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

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

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

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

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

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

557 
(*RA3*) 
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

558 
by (full_simp_tac (!simpset addsimps [parts_insert_sees]) 3 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

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

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

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

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

564 
qed "Cert_imp_Server_msg"; 