author  paulson 
Fri, 11 Jul 1997 13:26:15 +0200  
changeset 3512  9dcb4daa15e8 
parent 3483  6988394a6008 
child 3516  470626799511 
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 \ 
6988394a6008
Tidying; also simplified the lemma Says_Server_not
paulson
parents:
3466
diff
changeset

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}, \ 
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 ] \ 
6988394a6008
Tidying; also simplified the lemma Says_Server_not
paulson
parents:
3466
diff
changeset

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

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 ] \ 
3483
6988394a6008
Tidying; also simplified the lemma Says_Server_not
paulson
parents:
3466
diff
changeset

57 
\ ==> EX K. EX NA. EX evs: recur lost. \ 
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 
(*Monotonicity*) 

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

79 
by (rtac subsetI 1); 

80 
by (etac recur.induct 1); 

81 
by (REPEAT_FIRST 

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

82 
(blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono) 
2449  83 
:: recur.intrs)))); 
84 
qed "recur_mono"; 

85 

86 
(*Nobody sends themselves messages*) 

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

90 
qed_spec_mp "not_Says_to_self"; 

91 
Addsimps [not_Says_to_self]; 

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

93 

94 

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

95 

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

96 
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

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

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

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

100 

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

101 
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

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

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

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

105 

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

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

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

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

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

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

111 
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

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

113 
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

114 

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

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

118 
by (REPEAT (ares_tac (respond_imp_not_used::responses.intrs) 1)); 
2449  119 
qed "respond_imp_responses"; 
120 

121 

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

123 

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

124 
val RA2_analz_sees_Spy = Says_imp_sees_Spy RS analz.Inj > standard; 
2449  125 

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

128 
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

129 
qed "RA4_analz_sees_Spy"; 
2449  130 

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

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

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

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

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

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

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

139 
RA4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); 
2449  140 

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

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

142 
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

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

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

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

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

148 
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

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

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

151 
prove_simple_subgoals_tac 1 
2449  152 
end; 
153 

154 

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

156 
sends messages containing X! **) 

157 

158 

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

160 

161 
goal thy 

162 
"!!evs. evs : recur lost \ 

163 
\ ==> (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

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

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

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

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

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

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

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

171 
by (blast_tac (!claset addSEs partsEs addDs [parts_cut]) 1); 
2449  172 
qed "Spy_see_shrK"; 
173 
Addsimps [Spy_see_shrK]; 

174 

175 
goal thy 

176 
"!!evs. evs : recur lost \ 

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

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

179 
qed "Spy_analz_shrK"; 

180 
Addsimps [Spy_analz_shrK]; 

181 

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

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

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

184 
by (blast_tac (!claset addDs [Spy_see_shrK]) 1); 
2449  185 
qed "Spy_see_shrK_D"; 
186 

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

188 
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; 

189 

190 

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

191 

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

192 
(** Nobody can have used nonexistent keys! **) 
2449  193 

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

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

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

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

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

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

200 
qed_spec_mp "Key_in_keysFor_parts"; 
2449  201 

202 

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

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

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

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

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

207 
by (best_tac (!claset addDs [Key_in_keysFor_parts] 
3207  208 
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

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

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

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

212 
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

213 
impOfSubs (parts_insert_subset_Un RS keysFor_mono)] 
3207  214 
addss (!simpset)) 1); 
2449  215 
qed_spec_mp "new_keys_not_used"; 
216 

217 

218 
bind_thm ("new_keys_not_analzd", 

219 
[analz_subset_parts RS keysFor_mono, 

220 
new_keys_not_used] MRS contra_subsetD); 

221 

222 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 

223 

224 

225 

226 
(*** Proofs involving analz ***) 

227 

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

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

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

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

233 
dres_inst_tac [("lost","lost")] RA4_analz_sees_Spy 6; 
2449  234 

235 

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

237 

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

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

241 
goal thy 

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

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

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

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

245 
\ (K : KK  Key K : analz H) ] \ 
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 (insert RB (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 (insert RB H))"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

250 
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

251 
qed "resp_analz_image_freshK_lemma"; 
2449  252 

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

254 
goal thy 

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

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

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

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

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

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

261 
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

262 
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

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

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

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

267 
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

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

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

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

271 
qed_spec_mp "analz_image_freshK"; 
2449  272 

273 

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

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

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

277 
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

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

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

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

282 
(2, resp_analz_image_freshK_lemma) RS spec RS spec); 
2449  283 

284 
goal thy 

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

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

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

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

288 
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

289 
qed "analz_insert_freshK"; 
2449  290 

291 

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

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

293 
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

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

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

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

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

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

299 
by (etac responses.induct 2); 
2449  300 
by (ALLGOALS Asm_simp_tac); 
301 
(*Fake*) 

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

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

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

304 
qed "Hash_imp_body"; 
2449  305 

306 

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

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

309 

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

310 
Unicity is not used in other proofs but is desirable in its own right. 
2449  311 
**) 
312 

313 
goal thy 

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

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

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

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

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

319 
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

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

321 
by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib]))); 
2449  322 
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

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

324 
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

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

326 
by (REPEAT (blast_tac (!claset addSDs [Hash_imp_body] 
3483
6988394a6008
Tidying; also simplified the lemma Says_Server_not
paulson
parents:
3466
diff
changeset

327 
addSEs sees_Spy_partsEs) 1)); 
2449  328 
val lemma = result(); 
329 

2481  330 
goalw thy [HPair_def] 
3483
6988394a6008
Tidying; also simplified the lemma Says_Server_not
paulson
parents:
3466
diff
changeset

331 
"!!A.[ Hash[Key(shrK A)] {Agent A, B,NA,P} : parts(sees lost Spy evs); \ 
6988394a6008
Tidying; also simplified the lemma Says_Server_not
paulson
parents:
3466
diff
changeset

332 
\ Hash[Key(shrK A)] {Agent A, B',NA,P'} : parts(sees lost Spy evs); \ 
6988394a6008
Tidying; also simplified the lemma Says_Server_not
paulson
parents:
3466
diff
changeset

333 
\ evs : recur lost; A ~: lost ] \ 
6988394a6008
Tidying; also simplified the lemma Says_Server_not
paulson
parents:
3466
diff
changeset

334 
\ ==> B=B' & P=P'"; 
2481  335 
by (REPEAT (eresolve_tac partsEs 1)); 
2449  336 
by (prove_unique_tac lemma 1); 
337 
qed "unique_NA"; 

338 

339 

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

341 
(relations "respond" and "responses") 

342 
***) 

343 

344 
goal thy 

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

345 
"!!evs. [ RB : responses evs; evs : recur lost ] \ 
2449  346 
\ ==> (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

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 [Spy_analz_shrK, 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

351 
resp_analz_image_freshK]))); 
2449  352 
qed "shrK_in_analz_respond"; 
353 
Addsimps [shrK_in_analz_respond]; 

354 

355 

356 
goal thy 

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

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

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

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

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

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

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

363 
by (etac responses.induct 1); 
2449  364 
by (ALLGOALS 
365 
(asm_simp_tac 

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

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

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

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

369 
by (blast_tac (!claset delrules [allE]) 1); 
2449  370 
qed "resp_analz_insert_lemma"; 
371 

372 
bind_thm ("resp_analz_insert", 

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

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

374 
(2, resp_analz_insert_lemma) RSN(2, rev_mp)); 
2449  375 

376 

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

378 
assuming B~=Server in RA4.*) 
2449  379 
goal thy 
3483
6988394a6008
Tidying; also simplified the lemma Says_Server_not
paulson
parents:
3466
diff
changeset

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

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

383 
by (etac (respond.induct) 5); 
2449  384 
by (Auto_tac()); 
385 
qed_spec_mp "Says_Server_not"; 

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

387 

388 

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

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

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

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

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

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

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

396 

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

397 

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

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

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

403 
by (etac respond.induct 1); 
2449  404 
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [all_conj_distrib]))); 
405 
(*Base case*) 

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

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

408 
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

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

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

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

413 
by (expand_case_tac "K = KAB" 1); 
2449  414 
by (REPEAT (ares_tac [exI] 2)); 
415 
by (ex_strip_tac 1); 

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

416 
by (dtac respond_certificate 1); 
2449  417 
by (Fast_tac 1); 
418 
val lemma = result(); 

419 

420 
goal thy 

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

428 

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

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

432 

433 
goal thy 

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

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

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

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

443 
(analz_image_freshK_ss addsimps 
2533  444 
[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

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

446 
by (blast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1); 
2449  447 
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

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

449 
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

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

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

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

453 
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

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

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

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

457 
by (Blast_tac 1); 
2533  458 
qed_spec_mp "respond_Spy_not_see_session_key"; 
2449  459 

460 

461 
goal thy 

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

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

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

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

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

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

468 
by analz_sees_tac; 
2449  469 
by (ALLGOALS 
470 
(asm_simp_tac 

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

473 
(*RA4*) 
2533  474 
by (spy_analz_tac 5); 
475 
(*RA2*) 

476 
by (spy_analz_tac 3); 

2449  477 
(*Fake*) 
2533  478 
by (spy_analz_tac 2); 
479 
(*Base*) 

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

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

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

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

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

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

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

488 
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

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

490 
qed "Spy_not_see_session_key"; 
2449  491 

492 

493 
goal thy 

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

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

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

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

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

2533  501 
by (FIRSTGOAL (rtac Spy_not_see_session_key)); 
502 
by (REPEAT_FIRST 

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

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

504 
(!claset addIs (map impOfSubs [recur_mono, parts_mono, sees_mono])))); 
2533  505 
qed "Agent_not_see_session_key"; 
2449  506 

507 

508 
(**** Authenticity properties for Agents ****) 

509 

2481  510 
(*The response never contains Hashes*) 
511 
goal thy 

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

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

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

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

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

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

518 
qed "Hash_in_parts_respond"; 
2481  519 

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

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

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

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

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

527 
\ A ~: lost; evs : recur lost ] \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

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

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

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

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

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

533 
by (blast_tac (!claset addSDs [Hash_in_parts_respond]) 1); 
2449  534 
qed_spec_mp "Hash_auth_sender"; 
535 

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

536 
(** These two results subsume (for all agents) the guarantees proved 
2449  537 
separately for A and B in the OtwayRees protocol. 
538 
**) 

539 

540 

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

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

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

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

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

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

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

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

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

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

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

553 
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

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

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

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

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

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

559 
qed "Cert_imp_Server_msg"; 