author  paulson 
Thu, 26 Sep 1996 12:50:48 +0200  
changeset 2032  1bbf1bdcaf56 
parent 2026  0df5a96bf77e 
child 2045  ae1030e66745 
permissions  rwrr 
1934  1 
(* Title: HOL/Auth/Message 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1996 University of Cambridge 

5 

6 
Theory of Shared Keys (common to all symmetrickey protocols) 

7 

8 
Server keys; initial states of agents; new nonces and keys; function "sees" 

2032  9 
*) 
10 

1934  11 

12 

2032  13 
(****************DELETE****************) 
1934  14 

2032  15 
local 
16 
fun string_of (a,0) = a 

17 
 string_of (a,i) = a ^ "_" ^ string_of_int i; 

18 
in 

19 
fun freeze_thaw th = 

20 
let val fth = freezeT th 

21 
val {prop,sign,...} = rep_thm fth 

22 
fun mk_inst (Var(v,T)) = 

23 
(cterm_of sign (Var(v,T)), 

24 
cterm_of sign (Free(string_of v, T))) 

25 
val insts = map mk_inst (term_vars prop) 

26 
fun thaw th' = 

27 
th' > forall_intr_list (map #2 insts) 

28 
> forall_elim_list (map #1 insts) 

29 
in (instantiate ([],insts) fth, thaw) end; 

30 
end; 

31 
fun defer_tac i state = 

32 
let val (state',thaw) = freeze_thaw state 

33 
val hyps = Drule.strip_imp_prems (adjust_maxidx (cprop_of state')) 

34 
val hyp::hyps' = drop(i1,hyps) 

35 
in implies_intr hyp (implies_elim_list state' (map assume hyps)) 

36 
> implies_intr_list (take(i1,hyps) @ hyps') 

37 
> thaw 

38 
> Sequence.single 

39 
end 

40 
handle Bind => Sequence.null; 

41 

42 

43 

1934  44 

2000  45 
(*GOALS.ML??*) 
46 
fun prlim n = (goals_limit:=n; pr()); 

47 

1934  48 
(*FUN.ML?? WE NEED A NOTION OF INVERSE IMAGE, OR GRAPH!!*) 
49 
goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})"; 

50 
by (fast_tac (!claset addEs [equalityE]) 1); 

51 
val subset_range_iff = result(); 

52 

53 

54 
open Shared; 

55 

1964  56 
(*Holds because Friend is injective: thus cannot prove for all f*) 
57 
goal thy "(Friend x : Friend``A) = (x:A)"; 

58 
by (Auto_tac()); 

59 
qed "Friend_image_eq"; 

60 
Addsimps [Friend_image_eq]; 

61 

1934  62 
Addsimps [Un_insert_left, Un_insert_right]; 
63 

64 
(*By default only o_apply is builtin. But in the presence of etaexpansion 

65 
this means that some terms displayed as (f o g) will be rewritten, and others 

66 
will not!*) 

67 
Addsimps [o_def]; 

68 

1943  69 
(*** Basic properties of shrK and newK ***) 
1934  70 

1943  71 
(* invKey (shrK A) = shrK A *) 
72 
bind_thm ("invKey_shrK", rewrite_rule [isSymKey_def] isSym_shrK); 

1934  73 

74 
(* invKey (newK evs) = newK evs *) 

75 
bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK); 

1943  76 
Addsimps [invKey_shrK, invKey_newK]; 
1934  77 

78 

1993  79 
(*Injectiveness and freshness of new keys and nonces*) 
2032  80 
AddIffs [inj_shrK RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq]; 
1934  81 

82 
(** Rewrites should not refer to initState(Friend i) 

83 
 not in normal form! **) 

84 

1943  85 
Addsimps [newK_neq_shrK, newK_neq_shrK RS not_sym]; 
1934  86 

2032  87 
goal thy "Key (newK evs) ~: parts (initState lost B)"; 
88 
by (agent.induct_tac "B" 1); 

1934  89 
by (Auto_tac ()); 
2032  90 
qed "newK_notin_initState"; 
1934  91 

2032  92 
goal thy "Nonce (newN evs) ~: parts (initState lost B)"; 
93 
by (agent.induct_tac "B" 1); 

1934  94 
by (Auto_tac ()); 
2032  95 
qed "newN_notin_initState"; 
1934  96 

2032  97 
AddIffs [newK_notin_initState, newN_notin_initState]; 
1934  98 

2032  99 
goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}"; 
1934  100 
by (agent.induct_tac "C" 1); 
1993  101 
by (auto_tac (!claset addIs [range_eqI], !simpset)); 
1934  102 
qed "keysFor_parts_initState"; 
103 
Addsimps [keysFor_parts_initState]; 

104 

105 
goalw thy [keysFor_def] "keysFor (Key``E) = {}"; 

106 
by (Auto_tac ()); 

107 
qed "keysFor_image_Key"; 

108 
Addsimps [keysFor_image_Key]; 

109 

1943  110 
goal thy "shrK A ~: newK``E"; 
1934  111 
by (agent.induct_tac "A" 1); 
112 
by (Auto_tac ()); 

1943  113 
qed "shrK_notin_image_newK"; 
114 
Addsimps [shrK_notin_image_newK]; 

1934  115 

2032  116 

117 
(*** Function "sees" ***) 

118 

119 
goal thy 

120 
"!!evs. lost' <= lost ==> sees lost' A evs <= sees lost A evs"; 

121 
by (list.induct_tac "evs" 1); 

122 
by (agent.induct_tac "A" 1); 

123 
by (event.induct_tac "a" 2); 

124 
by (Auto_tac ()); 

125 
qed "sees_mono"; 

126 

1964  127 
(*Agents see their own shared keys!*) 
2032  128 
goal thy "A ~= Spy > Key (shrK A) : sees lost A evs"; 
1934  129 
by (list.induct_tac "evs" 1); 
130 
by (agent.induct_tac "A" 1); 

2032  131 
by (Auto_tac ()); 
132 
qed_spec_mp "sees_own_shrK"; 

1934  133 

2032  134 
(*Spy sees shared keys of lost agents!*) 
135 
goal thy "!!i. A: lost ==> Key (shrK A) : sees lost Spy evs"; 

136 
by (list.induct_tac "evs" 1); 

137 
by (Auto_tac()); 

138 
qed "Spy_sees_bad"; 

1934  139 

2032  140 
AddSIs [sees_own_shrK, Spy_sees_bad]; 
141 

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

142 

2032  143 
(** Specialized rewrite rules for (sees lost A (Says...#evs)) **) 
2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2012
diff
changeset

144 

2032  145 
goal thy "sees lost A (Says A B X # evs) = insert X (sees lost A evs)"; 
1934  146 
by (Simp_tac 1); 
147 
qed "sees_own"; 

148 

149 
goal thy "!!A. Server ~= A ==> \ 

2032  150 
\ sees lost Server (Says A B X # evs) = sees lost Server evs"; 
1934  151 
by (Asm_simp_tac 1); 
152 
qed "sees_Server"; 

153 

154 
goal thy "!!A. Friend i ~= A ==> \ 

2032  155 
\ sees lost (Friend i) (Says A B X # evs) = sees lost (Friend i) evs"; 
1934  156 
by (Asm_simp_tac 1); 
157 
qed "sees_Friend"; 

158 

2032  159 
goal thy "sees lost Spy (Says A B X # evs) = insert X (sees lost Spy evs)"; 
1934  160 
by (Simp_tac 1); 
2032  161 
qed "sees_Spy"; 
1934  162 

2032  163 
goal thy "sees lost A (Says A' B X # evs) <= insert X (sees lost A evs)"; 
1934  164 
by (simp_tac (!simpset setloop split_tac [expand_if]) 1); 
165 
by (Fast_tac 1); 

166 
qed "sees_Says_subset_insert"; 

167 

2032  168 
goal thy "sees lost A evs <= sees lost A (Says A' B X # evs)"; 
1934  169 
by (simp_tac (!simpset setloop split_tac [expand_if]) 1); 
170 
by (Fast_tac 1); 

171 
qed "sees_subset_sees_Says"; 

172 

2032  173 
(*Pushing Unions into parts; one of the A's equals B, and thus sees lost Y*) 
174 
goal thy "(UN A. parts (sees lost A (Says B C Y # evs))) = \ 

175 
\ parts {Y} Un (UN A. parts (sees lost A evs))"; 

1934  176 
by (Step_tac 1); 
2032  177 
by (etac rev_mp 1); (*for some reason, split_tac does not work on assumptions*) 
1934  178 
val ss = (!simpset addsimps [parts_Un, sees_Cons] 
2032  179 
setloop split_tac [expand_if]); 
1934  180 
by (ALLGOALS (fast_tac (!claset addss ss))); 
181 
qed "UN_parts_sees_Says"; 

182 

2032  183 
goal thy "Says A B X : set_of_list evs > X : sees lost Spy evs"; 
1934  184 
by (list.induct_tac "evs" 1); 
185 
by (Auto_tac ()); 

2032  186 
qed_spec_mp "Says_imp_sees_Spy"; 
1934  187 

2032  188 
Addsimps [Says_imp_sees_Spy]; 
189 
AddIs [Says_imp_sees_Spy]; 

1934  190 

2032  191 
goal thy "initState lost C <= Key `` range shrK"; 
1934  192 
by (agent.induct_tac "C" 1); 
193 
by (Auto_tac ()); 

194 
qed "initState_subset"; 

195 

2032  196 
goal thy "X : sees lost C evs > \ 
1934  197 
\ (EX A B. Says A B X : set_of_list evs)  \ 
1943  198 
\ (EX A. X = Key (shrK A))"; 
1934  199 
by (list.induct_tac "evs" 1); 
200 
by (ALLGOALS Asm_simp_tac); 

201 
by (fast_tac (!claset addDs [impOfSubs initState_subset]) 1); 

2032  202 
by (rtac conjI 1); 
1934  203 
by (Fast_tac 2); 
204 
by (event.induct_tac "a" 1); 

205 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [mem_if]))); 

206 
by (ALLGOALS Fast_tac); 

207 
qed_spec_mp "seesD"; 

208 

2032  209 
Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Spy]; 
210 
Delsimps [sees_Cons]; (**** NOTE REMOVAL  laws above are cleaner ****) 

1934  211 

212 

213 
goal thy "!!K. newK evs = invKey K ==> newK evs = K"; 

2032  214 
by (rtac (invKey_eq RS iffD1) 1); 
1934  215 
by (Simp_tac 1); 
216 
val newK_invKey = result(); 

217 

1993  218 
AddSDs [newK_invKey]; 
1934  219 

220 
(** Rewrites to push in Key and Crypt messages, so that other messages can 

221 
be pulled out using the analz_insert rules **) 

222 

223 
fun insComm x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)] 

224 
insert_commute; 

225 

226 
val pushKeys = map (insComm "Key ?K") 

227 
["Agent ?C", "Nonce ?N", "MPair ?X ?Y", "Crypt ?X ?K'"]; 

228 

229 
val pushCrypts = map (insComm "Crypt ?X ?K") 

230 
["Agent ?C", "Nonce ?N", "MPair ?X' ?Y"]; 

231 

232 
(*Cannot be added with Addsimps  we don't always want to reorder messages*) 

233 
val pushes = pushKeys@pushCrypts; 

234 

1943  235 
val pushKey_newK = insComm "Key (newK ?evs)" "Key (shrK ?C)"; 
1934  236 

237 

1993  238 
(*No premature instantiation of variables. For proving weak liveness.*) 
239 
fun safe_solver prems = 

240 
match_tac (TrueI::refl::prems) ORELSE' eq_assume_tac 

241 
ORELSE' etac FalseE; 

242 

2000  243 
(*Analysis of Fake cases and of messages that forward unknown parts 
244 
Abstraction over i is ESSENTIAL: it delays the dereferencing of claset*) 

2032  245 
fun spy_analz_tac i = 
1993  246 
SELECT_GOAL 
247 
(EVERY [ (*push in occurrences of X...*) 

2032  248 
(REPEAT o CHANGED) 
249 
(res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1), 

250 
(*...allowing further simplifications*) 

251 
simp_tac (!simpset setloop split_tac [expand_if]) 1, 

252 
REPEAT (resolve_tac [impI,notI] 1), 

253 
dtac (impOfSubs Fake_analz_insert) 1, 

254 
eresolve_tac [asm_rl, synth.Inj] 1, 

255 
Fast_tac 1, 

256 
Asm_full_simp_tac 1, 

257 
IF_UNSOLVED (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1) 

258 
]) i; 

1993  259 

260 

2032  261 
(** Simplifying parts (insert X (sees lost A evs)) 
262 
= parts {X} Un parts (sees lost A evs)  since general case loops*) 

2012  263 

264 
val parts_insert_sees = 

2032  265 
parts_insert > read_instantiate_sg (sign_of thy) [("H", "sees lost A evs")] 
2012  266 
> standard; 