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"


9 


10 


11 
*)


12 


13 
Addsimps [parts_cut_eq];


14 


15 
proof_timing:=true;


16 


17 
(*IN SET.ML*)


18 
goal Set.thy "(a : (if Q then x else y)) = ((Q > a:x) & (~Q > a : y))";


19 
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);


20 
qed "mem_if";


21 


22 
(*FUN.ML?? WE NEED A NOTION OF INVERSE IMAGE, OR GRAPH!!*)


23 
goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})";


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


25 
val subset_range_iff = result();


26 


27 


28 
open Shared;


29 


30 
Addsimps [Un_insert_left, Un_insert_right];


31 


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


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


34 
will not!*)


35 
Addsimps [o_def];


36 


37 
(*** Basic properties of serverKey and newK ***)


38 


39 
(* invKey (serverKey A) = serverKey A *)


40 
bind_thm ("invKey_serverKey", rewrite_rule [isSymKey_def] isSym_serverKey);


41 


42 
(* invKey (newK evs) = newK evs *)


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


44 
Addsimps [invKey_serverKey, invKey_newK];


45 


46 


47 
(*New keys and nonces are fresh*)


48 
val serverKey_inject = inj_serverKey RS injD;


49 
val newN_inject = inj_newN RS injD


50 
and newK_inject = inj_newK RS injD;


51 
AddSEs [serverKey_inject, newN_inject, newK_inject,


52 
fresh_newK RS notE, fresh_newN RS notE];


53 
Addsimps [inj_serverKey RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq];


54 
Addsimps [fresh_newN, fresh_newK];


55 


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


57 
 not in normal form! **)


58 


59 
goal thy "newK evs ~= serverKey B";


60 
by (subgoal_tac "newK evs = serverKey B > \


61 
\ Key (newK evs) : parts (initState B)" 1);


62 
by (Fast_tac 1);


63 
by (agent.induct_tac "B" 1);


64 
by (auto_tac (!claset addIs [range_eqI], !simpset));


65 
qed "newK_neq_serverKey";


66 


67 
Addsimps [newK_neq_serverKey, newK_neq_serverKey RS not_sym];


68 


69 
(*Good for talking about Server's initial state*)


70 
goal thy "!!H. H <= Key``E ==> parts H = H";


71 
by (Auto_tac ());


72 
be parts.induct 1;


73 
by (ALLGOALS (fast_tac (!claset addss (!simpset))));


74 
qed "parts_image_subset";


75 


76 
bind_thm ("parts_image_Key", subset_refl RS parts_image_subset);


77 


78 
goal thy "!!H. H <= Key``E ==> analz H = H";


79 
by (Auto_tac ());


80 
be analz.induct 1;


81 
by (ALLGOALS (fast_tac (!claset addss (!simpset))));


82 
qed "analz_image_subset";


83 


84 
bind_thm ("analz_image_Key", subset_refl RS analz_image_subset);


85 


86 
Addsimps [parts_image_Key, analz_image_Key];


87 


88 
goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";


89 
by (agent.induct_tac "C" 1);


90 
by (auto_tac (!claset addIs [range_eqI] delrules partsEs, !simpset));


91 
qed "keysFor_parts_initState";


92 
Addsimps [keysFor_parts_initState];


93 


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


95 
by (Auto_tac ());


96 
qed "keysFor_image_Key";


97 
Addsimps [keysFor_image_Key];


98 


99 
goal thy "serverKey A ~: newK``E";


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


101 
by (Auto_tac ());


102 
qed "serverKey_notin_image_newK";


103 
Addsimps [serverKey_notin_image_newK];


104 


105 


106 
(*Agents see their own serverKeys!*)


107 
goal thy "Key (serverKey A) : analz (sees A evs)";


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


109 
by (asm_simp_tac (!simpset addsimps [impOfSubs(Un_upper2 RS analz_mono)]) 2);


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


111 
by (auto_tac (!claset addIs [range_eqI], !simpset));


112 
qed "analz_own_serverKey";


113 


114 
bind_thm ("parts_own_serverKey",


115 
[analz_subset_parts, analz_own_serverKey] MRS subsetD);


116 


117 
Addsimps [analz_own_serverKey, parts_own_serverKey];


118 


119 


120 


121 
(** Specialized rewrite rules for (sees A (Says...#evs)) **)


122 


123 
goal thy "sees A (Says A B X # evs) = insert X (sees A evs)";


124 
by (Simp_tac 1);


125 
qed "sees_own";


126 


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


128 
\ sees Server (Says A B X # evs) = sees Server evs";


129 
by (Asm_simp_tac 1);


130 
qed "sees_Server";


131 


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


133 
\ sees (Friend i) (Says A B X # evs) = sees (Friend i) evs";


134 
by (Asm_simp_tac 1);


135 
qed "sees_Friend";


136 


137 
goal thy "sees Enemy (Says A B X # evs) = insert X (sees Enemy evs)";


138 
by (Simp_tac 1);


139 
qed "sees_Enemy";


140 


141 
goal thy "sees A (Says A' B X # evs) <= insert X (sees A evs)";


142 
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);


143 
by (Fast_tac 1);


144 
qed "sees_Says_subset_insert";


145 


146 
goal thy "sees A evs <= sees A (Says A' B X # evs)";


147 
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);


148 
by (Fast_tac 1);


149 
qed "sees_subset_sees_Says";


150 


151 
(*Pushing Unions into parts; one of the A's equals B, and thus sees Y*)


152 
goal thy "(UN A. parts (sees A (Says B C Y # evs))) = \


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


154 
by (Step_tac 1);


155 
be rev_mp 1; (*for some reason, split_tac does not work on assumptions*)


156 
val ss = (!simpset addsimps [parts_Un, sees_Cons]


157 
setloop split_tac [expand_if]);


158 
by (ALLGOALS (fast_tac (!claset addss ss)));


159 
qed "UN_parts_sees_Says";


160 


161 
goal thy "Says A B X : set_of_list evs > X : sees Enemy evs";


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


163 
by (Auto_tac ());


164 
qed_spec_mp "Says_imp_sees_Enemy";


165 


166 
Addsimps [Says_imp_sees_Enemy];


167 
AddIs [Says_imp_sees_Enemy];


168 


169 
goal thy "initState C <= Key `` range serverKey";


170 
by (agent.induct_tac "C" 1);


171 
by (Auto_tac ());


172 
qed "initState_subset";


173 


174 
goal thy "X : sees C evs > \


175 
\ (EX A B. Says A B X : set_of_list evs)  \


176 
\ (EX A. Notes A X : set_of_list evs)  \


177 
\ (EX A. X = Key (serverKey A))";


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


179 
by (ALLGOALS Asm_simp_tac);


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


181 
br conjI 1;


182 
by (Fast_tac 2);


183 
by (event.induct_tac "a" 1);


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


185 
by (ALLGOALS Fast_tac);


186 
qed_spec_mp "seesD";


187 


188 


189 
Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Enemy];


190 
Delsimps [sees_Cons]; (**** NOTE REMOVAL  laws above are cleaner ****)


191 


192 


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


194 
br (invKey_eq RS iffD1) 1;


195 
by (Simp_tac 1);


196 
val newK_invKey = result();


197 


198 


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


200 
be pulled out using the analz_insert rules **)


201 


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


203 
insert_commute;


204 


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


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


207 


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


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


210 


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


212 
val pushes = pushKeys@pushCrypts;


213 


214 
val pushKey_newK = insComm "Key (newK ?evs)" "Key (serverKey ?C)";


215 


216 
