2274

1 
(* Title: HOL/Auth/WooLam


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1996 University of Cambridge


5 


6 
Inductive relation "woolam" for the WooLam protocol.


7 


8 
Simplified version from page 11 of


9 
Abadi and Needham. Prudent Engineering Practice for Cryptographic Protocols.


10 
IEEE Trans. S.E. 22(1), 1996, pages 615.


11 
*)


12 


13 
open WooLam;


14 


15 
proof_timing:=true;


16 
HOL_quantifiers := false;


17 
Pretty.setdepth 20;


18 


19 


20 
(*Weak liveness: there are traces that reach the end*)


21 
goal thy


22 
"!!A B. [ A ~= B; A ~= Server; B ~= Server ] \


23 
\ ==> EX NB. EX evs: woolam lost. \


24 
\ Says Server B (Crypt {Agent A, Nonce NB} (shrK B)) \


25 
\ : set_of_list evs";


26 
by (REPEAT (resolve_tac [exI,bexI] 1));


27 
by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS


28 
woolam.WL4 RS woolam.WL5) 2);


29 
by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));


30 
by (REPEAT_FIRST (resolve_tac [refl, conjI]));


31 
by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver))));


32 
result();


33 


34 


35 
(**** Inductive proofs about woolam ****)


36 


37 
(*Nobody sends themselves messages*)


38 
goal thy "!!evs. evs : woolam lost ==> ALL A X. Says A A X ~: set_of_list evs";


39 
by (etac woolam.induct 1);


40 
by (Auto_tac());


41 
qed_spec_mp "not_Says_to_self";


42 
Addsimps [not_Says_to_self];


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


44 


45 


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


47 


48 
goal thy "!!evs. Says A' B X : set_of_list evs \


49 
\ ==> X : analz (sees lost Spy evs)";


50 
by (etac (Says_imp_sees_Spy RS analz.Inj) 1);


51 
qed "WL4_analz_sees_Spy";


52 


53 
bind_thm ("WL4_parts_sees_Spy",


54 
WL4_analz_sees_Spy RS (impOfSubs analz_subset_parts));


55 


56 
(*We instantiate the variable to "lost". Leaving it as a Var makes proofs


57 
harder to complete, since simplification does less for us.*)


58 
val parts_Fake_tac = forw_inst_tac [("lost","lost")] WL4_parts_sees_Spy 6;


59 


60 
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)


61 
fun parts_induct_tac i = SELECT_GOAL


62 
(DETERM (etac woolam.induct 1 THEN parts_Fake_tac THEN


63 
(*Fake message*)


64 
TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,


65 
impOfSubs Fake_parts_insert]


66 
addss (!simpset)) 2)) THEN


67 
(*Base case*)


68 
fast_tac (!claset addss (!simpset)) 1 THEN


69 
ALLGOALS Asm_simp_tac) i;


70 


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


72 
sends messages containing X! **)


73 


74 
(*Spy never sees another agent's shared key! (unless it's lost at start)*)


75 
goal thy


76 
"!!evs. evs : woolam lost \


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


78 
by (parts_induct_tac 1);


79 
by (Auto_tac());


80 
qed "Spy_see_shrK";


81 
Addsimps [Spy_see_shrK];


82 


83 
goal thy


84 
"!!evs. evs : woolam lost \


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


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


87 
qed "Spy_analz_shrK";


88 
Addsimps [Spy_analz_shrK];


89 


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


91 
\ evs : woolam lost ] ==> A:lost";


92 
by (fast_tac (!claset addDs [Spy_see_shrK]) 1);


93 
qed "Spy_see_shrK_D";


94 


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


96 
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];


97 


98 


99 
(*** Future nonces can't be seen or used! ***)


100 


101 
goal thy "!!evs. evs : woolam lost ==> \


102 
\ length evs <= length evt > \


103 
\ Nonce (newN evt) ~: parts (sees lost Spy evs)";


104 
by (parts_induct_tac 1);


105 
by (REPEAT_FIRST (fast_tac (!claset


106 
addSEs partsEs


107 
addSDs [Says_imp_sees_Spy RS parts.Inj]


108 
addEs [leD RS notE]


109 
addDs [impOfSubs analz_subset_parts,


110 
impOfSubs parts_insert_subset_Un,


111 
Suc_leD]


112 
addss (!simpset))));


113 
qed_spec_mp "new_nonces_not_seen";


114 
Addsimps [new_nonces_not_seen];


115 


116 


117 
(**** Autheticity properties for WooLam ****)


118 


119 


120 
(*** WL4 ***)


121 


122 
(*If the encrypted message appears then it originated with Alice*)


123 
goal thy


124 
"!!evs. [ A ~: lost; evs : woolam lost ] \


125 
\ ==> Crypt (Nonce NB) (shrK A) : parts (sees lost Spy evs) \


126 
\ > (EX B. Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs)";


127 
by (parts_induct_tac 1);


128 
by (Fast_tac 1);


129 
qed_spec_mp "NB_Crypt_imp_Alice_msg";


130 


131 
(*Guarantee for Server: if it gets a message containing a certificate from


132 
Alice, then she originated that certificate. But we DO NOT know that B


133 
ever saw it: the Spy may have rerouted the message to the Server.*)


134 
goal thy


135 
"!!evs. [ A ~: lost; evs : woolam lost; \


136 
\ Says B' Server {Agent A, Agent B, Crypt (Nonce NB) (shrK A)} \


137 
\ : set_of_list evs ] \


138 
\ ==> EX B. Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs";


139 
by (fast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg]


140 
addSEs [MPair_parts]


141 
addDs [Says_imp_sees_Spy RS parts.Inj]) 1);


142 
qed "Server_trust_WL4";


143 


144 


145 
(*** WL5 ***)


146 


147 
(*Server sent WL5 only if it received the right sort of message*)


148 
goal thy


149 
"!!evs. evs : woolam lost ==> \


150 
\ Says Server B (Crypt {Agent A, NB} (shrK B)) : set_of_list evs \


151 
\ > (EX B'. Says B' Server {Agent A, Agent B, Crypt NB (shrK A)} \


152 
\ : set_of_list evs)";


153 
by (parts_induct_tac 1);


154 
by (ALLGOALS Fast_tac);


155 
bind_thm ("Server_sent_WL5", result() RSN (2, rev_mp));


156 


157 


158 
(*If the encrypted message appears then it originated with the Server!*)


159 
goal thy


160 
"!!evs. [ B ~: lost; evs : woolam lost ] \


161 
\ ==> Crypt {Agent A, NB} (shrK B) : parts (sees lost Spy evs) \


162 
\ > Says Server B (Crypt {Agent A, NB} (shrK B)) : set_of_list evs";


163 
by (parts_induct_tac 1);


164 
qed_spec_mp "NB_Crypt_imp_Server_msg";


165 


166 
(*Partial guarantee for B: if it gets a message of correct form then the Server


167 
sent the same message.*)


168 
goal thy


169 
"!!evs. [ Says S B (Crypt {Agent A, NB} (shrK B)) : set_of_list evs; \


170 
\ B ~: lost; evs : woolam lost ] \


171 
\ ==> Says Server B (Crypt {Agent A, NB} (shrK B)) : set_of_list evs";


172 
by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]


173 
addDs [Says_imp_sees_Spy RS parts.Inj]) 1);


174 
qed "B_got_WL5";


175 


176 
(*Guarantee for B. If B gets the Server's certificate then A has encrypted


177 
the nonce using her key. This event can be no older than the nonce itself.


178 
But A may have sent the nonce to some other agent and it could have reached


179 
the Server via the Spy.*)


180 
goal thy


181 
"!!evs. [ Says S B (Crypt {Agent A, Nonce NB} (shrK B)): set_of_list evs; \


182 
\ A ~: lost; B ~: lost; evs : woolam lost ] \


183 
\ ==> EX B. Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs";


184 
by (fast_tac (!claset addIs [Server_trust_WL4]


185 
addSDs [B_got_WL5 RS Server_sent_WL5]) 1);


186 
qed "B_trust_WL5";


187 


188 


189 
(*B only issues challenges in response to WL1. Useful??*)


190 
goal thy


191 
"!!evs. [ B ~= Spy; evs : woolam lost ] \


192 
\ ==> Says B A (Nonce NB) : set_of_list evs \


193 
\ > (EX A'. Says A' B (Agent A) : set_of_list evs)";


194 
by (parts_induct_tac 1);


195 
by (ALLGOALS Fast_tac);


196 
bind_thm ("B_said_WL2", result() RSN (2, rev_mp));


197 


198 


199 
(**CANNOT be proved because A doesn't know where challenges come from...


200 
goal thy


201 
"!!evs. [ A ~: lost; B ~= Spy; evs : woolam lost ] \


202 
\ ==> Crypt (Nonce NB) (shrK A) : parts (sees lost Spy evs) & \


203 
\ Says B A (Nonce NB) : set_of_list evs \


204 
\ > Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs";


205 
by (parts_induct_tac 1);


206 
by (Step_tac 1);


207 
by (best_tac (!claset addSEs partsEs


208 
addEs [new_nonces_not_seen RSN(2,rev_notE)]) 1);


209 
**)
