author  paulson 
Wed, 21 Jul 1999 15:22:11 +0200  
changeset 7057  b9ddbb925939 
parent 5535  678999604ee9 
child 7499  23e090051cb8 
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 

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

9 
Pretty.setdepth 30; 
2449  10 

5359  11 
AddEs spies_partsEs; 
12 
AddDs [impOfSubs analz_subset_parts]; 

13 
AddDs [impOfSubs Fake_parts_insert]; 

14 

15 

2449  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*) 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

23 
Goal "EX K NA. EX evs: recur. \ 
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

24 
\ Says Server A {Crypt (shrK A) {Key K, Agent Server, Nonce NA}, \ 
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

25 
\ END} : set evs"; 
2449  26 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

27 
by (rtac (recur.Nil RS recur.RA1 RS (respond.One RSN (3,recur.RA3))) 2); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

28 
by possibility_tac; 
2449  29 
result(); 
30 

31 

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

5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

33 
Goal "EX K. EX NA. EX evs: recur. \ 
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

34 
\ Says B A {Crypt (shrK A) {Key K, Agent B, Nonce NA}, \ 
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

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

36 
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

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

39 
by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

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

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

42 
by basic_possibility_tac; 
5351  43 
by (DEPTH_SOLVE (eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1)); 
2449  44 
result(); 
45 

46 

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

47 
(*Case three: Alice, Bob, Charlie and the server 
2533  48 
TOO SLOW to run every time! 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

49 
Goal "EX K. EX NA. EX evs: recur. \ 
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

50 
\ Says B A {Crypt (shrK A) {Key K, Agent B, Nonce NA}, \ 
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

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

52 
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

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

55 
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

56 
(respond.One RS respond.Cons RS respond.Cons RSN 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

57 
(3,recur.RA3)) RS recur.RA4 RS recur.RA4) 2); 
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

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

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

60 
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

61 
ORELSE 
5351  62 
eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1)); 
2449  63 
result(); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

64 
****************) 
2449  65 

66 
(**** Inductive proofs about recur ****) 

67 

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

68 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

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

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

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

73 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

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

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

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

78 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

79 
Goal "[ Key K : parts {RB}; (PB,RB,K') : respond evs ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

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

82 
by (etac respond.induct 1); 
4091  83 
by (auto_tac(claset() addDs [Key_not_used, respond_imp_not_used], 
84 
simpset())); 

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

85 
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

86 

2449  87 
(*Simple inductive reasoning about responses*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

90 
by (REPEAT (ares_tac (respond_imp_not_used::responses.intrs) 1)); 
2449  91 
qed "respond_imp_responses"; 
92 

93 

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

95 

3683  96 
val RA2_analz_spies = Says_imp_spies RS analz.Inj > standard; 
2449  97 

5359  98 
Goal "Says C' B {Crypt K X, X', RA} : set evs ==> RA : analz (spies evs)"; 
4091  99 
by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1); 
3683  100 
qed "RA4_analz_spies"; 
2449  101 

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

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

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

3683  107 
bind_thm ("RA2_parts_spies", 
108 
RA2_analz_spies RS (impOfSubs analz_subset_parts)); 

109 
bind_thm ("RA4_parts_spies", 

110 
RA4_analz_spies RS (impOfSubs analz_subset_parts)); 

2449  111 

3683  112 
(*For proving the easier theorems about X ~: parts (spies evs).*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

113 
fun parts_induct_tac i = 
5359  114 
EVERY [etac recur.induct i, 
115 
forward_tac [RA4_parts_spies] (i+5), 

116 
forward_tac [respond_imp_responses] (i+4), 

117 
forward_tac [RA2_parts_spies] (i+3), 

118 
prove_simple_subgoals_tac i]; 

2449  119 

120 

3683  121 
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY 
2449  122 
sends messages containing X! **) 
123 

124 

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

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

127 
Goal "evs : recur ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

128 
by (parts_induct_tac 1); 
5359  129 
by Auto_tac; 
2550
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

130 
(*RA3*) 
5359  131 
by (auto_tac (claset() addDs [Key_in_parts_respond], 
132 
simpset() addsimps [parts_insert_spies])); 

2449  133 
qed "Spy_see_shrK"; 
134 
Addsimps [Spy_see_shrK]; 

135 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

136 
Goal "evs : recur ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; 
5359  137 
by Auto_tac; 
2449  138 
qed "Spy_analz_shrK"; 
139 
Addsimps [Spy_analz_shrK]; 

140 

4471  141 
AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
142 
Spy_analz_shrK RSN (2, rev_iffD1)]; 

2449  143 

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

144 

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

145 
(** Nobody can have used nonexistent keys! **) 
2449  146 

4509
828148415197
Making proofs faster, especially using keysFor_parts_insert
paulson
parents:
4477
diff
changeset

147 
(*The special case of H={} has the same proof*) 
5359  148 
Goal "[ K : keysFor (parts (insert RB H)); RB : responses evs ] \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

149 
\ ==> K : range shrK  K : keysFor (parts H)"; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

150 
by (etac rev_mp 1); 
5359  151 
by (etac responses.induct 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4471
diff
changeset

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

153 
qed_spec_mp "Key_in_keysFor_parts"; 
2449  154 

155 

5359  156 
Goal "evs : recur ==> Key K ~: used evs > K ~: keysFor (parts (spies evs))"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

159 
by (blast_tac (claset() addSDs [Key_in_keysFor_parts]) 2); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

161 
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); 
2449  162 
qed_spec_mp "new_keys_not_used"; 
163 

164 

165 
bind_thm ("new_keys_not_analzd", 

166 
[analz_subset_parts RS keysFor_mono, 

167 
new_keys_not_used] MRS contra_subsetD); 

168 

169 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 

170 

171 

172 

173 
(*** Proofs involving analz ***) 

174 

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

175 
(*For proofs involving analz.*) 
3683  176 
val analz_spies_tac = 
177 
dtac RA2_analz_spies 4 THEN 

2449  178 
forward_tac [respond_imp_responses] 5 THEN 
3683  179 
dtac RA4_analz_spies 6; 
2449  180 

181 

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

183 

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

184 
(*Version for "responses" relation. Handles case RA3 in the theorem below. 
3683  185 
Note that it holds for *any* set H (not just "spies evs") 
2449  186 
satisfying the inductive hypothesis.*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

187 
Goal "[ RB : responses evs; \ 
5492  188 
\ ALL K KK. KK <=  (range shrK) > \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

189 
\ (Key K : analz (Key``KK Un H)) = \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

190 
\ (K : KK  Key K : analz H) ] \ 
5492  191 
\ ==> ALL K KK. KK <=  (range shrK) > \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

192 
\ (Key K : analz (insert RB (Key``KK Un H))) = \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

193 
\ (K : KK  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

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

195 
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

196 
qed "resp_analz_image_freshK_lemma"; 
2449  197 

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

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

199 
Goal "evs : recur ==> \ 
5492  200 
\ ALL K KK. KK <=  (range shrK) > \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

201 
\ (Key K : analz (Key``KK Un (spies evs))) = \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

202 
\ (K : KK  Key K : analz (spies evs))"; 
2449  203 
by (etac recur.induct 1); 
3683  204 
by analz_spies_tac; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

205 
by (REPEAT_FIRST (resolve_tac [allI, impI])); 
4552
bb8ff763c93d
Simplified proofs by omitting PA = {XA, ...} from RA2
paulson
parents:
4509
diff
changeset

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

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

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

209 
(analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma]))); 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

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

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

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

213 
qed_spec_mp "analz_image_freshK"; 
2449  214 

215 

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

217 
[ RB : responses evs; evs : recur; ] 
5492  218 
==> KK <=  (range shrK) > 
3683  219 
Key K : analz (insert RB (Key``KK Un spies evs)) = 
220 
(K : KK  Key K : analz (insert RB (spies evs))) 

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

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

223 
raw_analz_image_freshK RSN 
3961  224 
(2, resp_analz_image_freshK_lemma) RS spec RS spec RS mp); 
2449  225 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

226 
Goal "[ evs : recur; KAB ~: range shrK ] ==> \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

227 
\ Key K : analz (insert (Key KAB) (spies evs)) = \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

229 
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

230 
qed "analz_insert_freshK"; 
2449  231 

232 

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

233 
(*Everything that's hashed is already in past traffic. *) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

234 
Goal "[ Hash {Key(shrK A), X} : parts (spies evs); \ 
5359  235 
\ evs : recur; A ~: bad ] ==> X : parts (spies evs)"; 
2550
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

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

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

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

239 
by (etac responses.induct 2); 
2449  240 
by (ALLGOALS Asm_simp_tac); 
241 
(*Fake*) 

5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

242 
by (blast_tac (claset() addIs [parts_insertI]) 1); 
2550
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2533
diff
changeset

243 
qed "Hash_imp_body"; 
2449  244 

245 

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

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

248 

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

249 
Unicity is not used in other proofs but is desirable in its own right. 
2449  250 
**) 
251 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

252 
Goal "[ evs : recur; A ~: bad ] \ 
2560  253 
\ ==> EX B' P'. ALL B P. \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

254 
\ Hash {Key(shrK A), Agent A, B, NA, P} : parts (spies evs) \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

255 
\ > B=B' & P=P'"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

258 
by (etac responses.induct 3); 
4091  259 
by (ALLGOALS (simp_tac (simpset() addsimps [all_conj_distrib]))); 
260 
by (clarify_tac (claset() addSEs partsEs) 1); 

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

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

262 
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

263 
by (REPEAT_FIRST (ares_tac [exI])); 
5359  264 
by (REPEAT (blast_tac (claset() addSDs [Hash_imp_body]) 1)); 
2449  265 
val lemma = result(); 
266 

5076  267 
Goalw [HPair_def] 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

268 
"[ Hash[Key(shrK A)] {Agent A, B,NA,P} : parts (spies evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

269 
\ Hash[Key(shrK A)] {Agent A, B',NA,P'} : parts (spies evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

270 
\ evs : recur; A ~: bad ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

271 
\ ==> B=B' & P=P'"; 
2481  272 
by (REPEAT (eresolve_tac partsEs 1)); 
2449  273 
by (prove_unique_tac lemma 1); 
274 
qed "unique_NA"; 

275 

276 

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

278 
(relations "respond" and "responses") 

279 
***) 

280 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

283 
by (etac responses.induct 1); 
2449  284 
by (ALLGOALS 
285 
(asm_simp_tac 

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

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

287 
resp_analz_image_freshK]))); 
2449  288 
qed "shrK_in_analz_respond"; 
289 
Addsimps [shrK_in_analz_respond]; 

290 

291 

5492  292 
Goal "[ RB : responses evs; \ 
293 
\ ALL K KK. KK <=  (range shrK) > \ 

294 
\ (Key K : analz (Key``KK Un H)) = \ 

295 
\ (K : KK  Key K : analz H) ] \ 

296 
\ ==> (Key K : analz (insert RB H)) > \ 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

298 
by (etac responses.induct 1); 
2449  299 
by (ALLGOALS 
300 
(asm_simp_tac 

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

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

302 
(*Simplification using two distinct treatments of "image"*) 
4091  303 
by (simp_tac (simpset() addsimps [parts_insert2]) 1); 
304 
by (blast_tac (claset() delrules [allE]) 1); 

2449  305 
qed "resp_analz_insert_lemma"; 
306 

307 
bind_thm ("resp_analz_insert", 

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

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

309 
(2, resp_analz_insert_lemma) RSN(2, rev_mp)); 
2449  310 

311 

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

312 
(*The last key returned by respond indeed appears in a certificate*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

313 
Goal "(Hash[Key(shrK A)] {Agent A, B, NA, P}, RA, K) : respond evs \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

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

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

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

318 

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

319 

5359  320 
Goal "(PB,RB,KXY) : respond evs \ 
321 
\ ==> EX A' B'. ALL A B N. \ 

322 
\ Crypt (shrK A) {Key K, Agent B, N} : parts {RB} \ 

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

324 
by (etac respond.induct 1); 
4091  325 
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [all_conj_distrib]))); 
2449  326 
(*Base case*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

329 
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

330 
by (dtac respond_Key_in_parts 1); 
4091  331 
by (blast_tac (claset() addSIs [exI] 
4598
649bf14debe7
Added some more explicit guarantees of key secrecy for agents
paulson
parents:
4556
diff
changeset

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

333 
by (expand_case_tac "K = KAB" 1); 
2449  334 
by (REPEAT (ares_tac [exI] 2)); 
335 
by (ex_strip_tac 1); 

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

336 
by (dtac respond_certificate 1); 
5359  337 
by (Blast_tac 1); 
2449  338 
val lemma = result(); 
339 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

340 
Goal "[ Crypt (shrK A) {Key K, Agent B, N} : parts {RB}; \ 
5359  341 
\ Crypt (shrK A') {Key K, Agent B', N'} : parts {RB}; \ 
342 
\ (PB,RB,KXY) : respond evs ] \ 

343 
\ ==> (A'=A & B'=B)  (A'=B & B'=A)"; 

2560  344 
by (prove_unique_tac lemma 1); 
2449  345 
qed "unique_session_keys"; 
346 

347 

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

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

351 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

352 
Goal "[ (PB,RB,KAB) : respond evs; evs : recur ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

353 
\ ==> ALL A A' N. A ~: bad & A' ~: bad > \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

354 
\ Crypt (shrK A) {Key K, Agent A', N} : parts{RB} > \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

355 
\ Key K ~: analz (insert RB (spies evs))"; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

358 
by (forward_tac [respond_imp_not_used] 2); 
3961  359 
by (ALLGOALS (*6 seconds*) 
2449  360 
(asm_simp_tac 
3961  361 
(analz_image_freshK_ss 
4831  362 
addsimps split_ifs 
3961  363 
addsimps 
364 
[shrK_in_analz_respond, resp_analz_image_freshK, parts_insert2]))); 

4091  365 
by (ALLGOALS (simp_tac (simpset() addsimps [ex_disj_distrib]))); 
3681  366 
(** LEVEL 5 **) 
5359  367 
by (Blast_tac 1); 
3961  368 
by (REPEAT_FIRST (resolve_tac [allI, conjI, impI])); 
369 
by (ALLGOALS Clarify_tac); 

4091  370 
by (blast_tac (claset() addSDs [resp_analz_insert] 
7057
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
5535
diff
changeset

371 
addIs [impOfSubs analz_subset_parts]) 3); 
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
5535
diff
changeset

372 
by (blast_tac (claset() addSDs [respond_certificate]) 2); 
3961  373 
by (Asm_full_simp_tac 1); 
374 
(*by unicity, either B=Aa or B=A', a contradiction if B: bad*) 

375 
by (blast_tac 

4091  376 
(claset() addSEs [MPair_parts] 
3961  377 
addDs [parts.Body, 
378 
respond_certificate RSN (2, unique_session_keys)]) 1); 

2533  379 
qed_spec_mp "respond_Spy_not_see_session_key"; 
2449  380 

381 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

382 
Goal "[ Crypt (shrK A) {Key K, Agent A', N} : parts (spies evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

383 
\ A ~: bad; A' ~: bad; evs : recur ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

385 
by (etac rev_mp 1); 
2449  386 
by (etac recur.induct 1); 
3683  387 
by analz_spies_tac; 
2449  388 
by (ALLGOALS 
389 
(asm_simp_tac 

5535  390 
(simpset() addsimps split_ifs @ [analz_insert_eq, analz_insert_freshK]))); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

391 
(*RA4*) 
2533  392 
by (spy_analz_tac 5); 
393 
(*RA2*) 

394 
by (spy_analz_tac 3); 

2449  395 
(*Fake*) 
2533  396 
by (spy_analz_tac 2); 
397 
(*Base*) 

7057
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
5535
diff
changeset

398 
by (Force_tac 1); 
2533  399 
(*RA3 remains*) 
4556
e7a4683c0026
Tidying, mostly to do with handling a more specific version of Fake_parts_insert
paulson
parents:
4552
diff
changeset

400 
by (simp_tac (simpset() addsimps [parts_insert_spies]) 1); 
4091  401 
by (safe_tac (claset() delrules [impCE])); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

402 
(*RA3, case 2: K is an old key*) 
4091  403 
by (blast_tac (claset() addSDs [resp_analz_insert] 
4556
e7a4683c0026
Tidying, mostly to do with handling a more specific version of Fake_parts_insert
paulson
parents:
4552
diff
changeset

404 
addSEs partsEs 
e7a4683c0026
Tidying, mostly to do with handling a more specific version of Fake_parts_insert
paulson
parents:
4552
diff
changeset

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

406 
(*RA3, case 1: use lemma previously proved by induction*) 
4091  407 
by (blast_tac (claset() addSEs [respond_Spy_not_see_session_key RSN 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

409 
qed "Spy_not_see_session_key"; 
2449  410 

411 
(**** Authenticity properties for Agents ****) 

412 

2481  413 
(*The response never contains Hashes*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

414 
Goal "[ Hash {Key (shrK B), M} : parts (insert RB H); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

415 
\ (PB,RB,K) : respond evs ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

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

418 
by (etac (respond_imp_responses RS responses.induct) 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4471
diff
changeset

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

420 
qed "Hash_in_parts_respond"; 
2481  421 

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

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

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

5076  426 
Goalw [HPair_def] 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

427 
"[ Hash {Key(shrK A), Agent A, Agent B, NA, P} : parts(spies evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

428 
\ A ~: bad; evs : recur ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

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

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

433 
(*RA3*) 
4091  434 
by (blast_tac (claset() addSDs [Hash_in_parts_respond]) 1); 
2449  435 
qed_spec_mp "Hash_auth_sender"; 
436 

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

437 
(** These two results subsume (for all agents) the guarantees proved 
2449  438 
separately for A and B in the OtwayRees protocol. 
439 
**) 

440 

441 

2533  442 
(*Certificates can only originate with the Server.*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

443 
Goal "[ Crypt (shrK A) Y : parts (spies evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

444 
\ A ~: bad; evs : recur ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

445 
\ ==> EX C RC. Says Server C RC : set evs & \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

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

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

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

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

452 
(*RA3*) 
4091  453 
by (full_simp_tac (simpset() addsimps [parts_insert_spies]) 3 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

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

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

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

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

459 
qed "Cert_imp_Server_msg"; 