6400

1 
(* Title: HOL/Auth/Yahalom


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1996 University of Cambridge


5 


6 
Inductive relation "yahalom" for the Yahalom protocol.


7 


8 
From page 257 of


9 
Burrows, Abadi and Needham. A Logic of Authentication.


10 
Proc. Royal Soc. 426 (1989)


11 
*)


12 


13 
(*A "possibility property": there are traces that reach the end*)


14 
Goal "A ~= Server \


15 
\ ==> EX X NB K. EX evs: yahalom. \


16 
\ Says A B {X, Crypt K (Nonce NB)} : set evs";


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


18 
by (rtac (yahalom.Nil RS


19 
yahalom.YM1 RS yahalom.Reception RS


20 
yahalom.YM2 RS yahalom.Reception RS


21 
yahalom.YM3 RS yahalom.Reception RS yahalom.YM4) 2);


22 
by possibility_tac;


23 
result();


24 


25 
Goal "[ Gets B X : set evs; evs : yahalom ] ==> EX A. Says A B X : set evs";


26 
by (etac rev_mp 1);


27 
by (etac yahalom.induct 1);


28 
by Auto_tac;


29 
qed "Gets_imp_Says";


30 


31 
(*Must be proved separately for each protocol*)


32 
Goal "[ Gets B X : set evs; evs : yahalom ] ==> X : knows Spy evs";


33 
by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1);


34 
qed"Gets_imp_knows_Spy";


35 
AddDs [Gets_imp_knows_Spy RS parts.Inj];


36 


37 
fun g_not_bad_tac s =

7499

38 
ftac Gets_imp_Says THEN' assume_tac THEN' not_bad_tac s;

6400

39 


40 


41 
(**** Inductive proofs about yahalom ****)


42 


43 


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


45 


46 
(*Lets us treat YM4 using a similar argument as for the Fake case.*)


47 
Goal "[ Gets A {Crypt (shrK A) Y, X} : set evs; evs : yahalom ] \


48 
\ ==> X : analz (knows Spy evs)";


49 
by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);


50 
qed "YM4_analz_knows_Spy";


51 


52 
bind_thm ("YM4_parts_knows_Spy",


53 
YM4_analz_knows_Spy RS (impOfSubs analz_subset_parts));


54 


55 
(*For proving the easier theorems about X ~: parts (knows Spy evs).*)


56 
fun parts_knows_Spy_tac i =


57 
EVERY

7499

58 
[ftac YM4_parts_knows_Spy (i+6), assume_tac (i+6),

6400

59 
prove_simple_subgoals_tac i];


60 


61 
(*Induction for regularity theorems. If induction formula has the form


62 
X ~: analz (knows Spy evs) > ... then it shortens the proof by discarding


63 
needless information about analz (insert X (knows Spy evs)) *)


64 
fun parts_induct_tac i =


65 
etac yahalom.induct i


66 
THEN


67 
REPEAT (FIRSTGOAL analz_mono_contra_tac)


68 
THEN parts_knows_Spy_tac i;


69 


70 


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


72 
sends messages containing X! **)


73 


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


75 
Goal "evs : yahalom ==> (Key (shrK A) : parts (knows Spy evs)) = (A : bad)";


76 
by (parts_induct_tac 1);


77 
by (Fake_parts_insert_tac 1);


78 
by (ALLGOALS Blast_tac);


79 
qed "Spy_see_shrK";


80 
Addsimps [Spy_see_shrK];


81 


82 
Goal "evs : yahalom ==> (Key (shrK A) : analz (knows Spy evs)) = (A : bad)";


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


84 
qed "Spy_analz_shrK";


85 
Addsimps [Spy_analz_shrK];


86 


87 
AddSDs [Spy_see_shrK RSN (2, rev_iffD1),


88 
Spy_analz_shrK RSN (2, rev_iffD1)];


89 


90 


91 
(*Nobody can have used nonexistent keys! Needed to apply analz_insert_Key*)


92 
Goal "evs : yahalom ==> \


93 
\ Key K ~: used evs > K ~: keysFor (parts (knows Spy evs))";


94 
by (parts_induct_tac 1);


95 
(*Fake*)


96 
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);


97 
(*YM24: Because Key K is not fresh, etc.*)


98 
by (REPEAT (blast_tac (claset() addSEs knows_Spy_partsEs) 1));


99 
qed_spec_mp "new_keys_not_used";


100 


101 
bind_thm ("new_keys_not_analzd",


102 
[analz_subset_parts RS keysFor_mono,


103 
new_keys_not_used] MRS contra_subsetD);


104 


105 
Addsimps [new_keys_not_used, new_keys_not_analzd];


106 


107 


108 
(*For proofs involving analz.*)


109 
val analz_knows_Spy_tac =

7499

110 
ftac YM4_analz_knows_Spy 7 THEN assume_tac 7;

6400

111 


112 
(****


113 
The following is to prove theorems of the form


114 


115 
Key K : analz (insert (Key KAB) (knows Spy evs)) ==>


116 
Key K : analz (knows Spy evs)


117 


118 
A more general formula must be proved inductively.


119 
****)


120 


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


122 


123 
Goal "evs : yahalom ==> \


124 
\ ALL K KK. KK <=  (range shrK) > \


125 
\ (Key K : analz (Key``KK Un (knows Spy evs))) = \


126 
\ (K : KK  Key K : analz (knows Spy evs))";


127 
by (etac yahalom.induct 1);


128 
by analz_knows_Spy_tac;


129 
by (REPEAT_FIRST (resolve_tac [allI, impI]));


130 
by (REPEAT_FIRST (rtac analz_image_freshK_lemma));


131 
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));


132 
(*Fake*)


133 
by (spy_analz_tac 1);


134 
qed_spec_mp "analz_image_freshK";


135 


136 
Goal "[ evs : yahalom; KAB ~: range shrK ] \


137 
\ ==> Key K : analz (insert (Key KAB) (knows Spy evs)) = \


138 
\ (K = KAB  Key K : analz (knows Spy evs))";


139 
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);


140 
qed "analz_insert_freshK";


141 


142 


143 
(*** The Key K uniquely identifies the Server's message. **)


144 


145 
Goal "evs : yahalom ==> \


146 
\ EX A' B' na' nb' X'. ALL A B na nb X. \


147 
\ Says Server A \


148 
\ {Crypt (shrK A) {Agent B, Key K, na, nb}, X} \


149 
\ : set evs > A=A' & B=B' & na=na' & nb=nb' & X=X'";


150 
by (etac yahalom.induct 1);


151 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));


152 
by (ALLGOALS Clarify_tac);


153 
by (ex_strip_tac 2);


154 
by (Blast_tac 2);


155 
(*Remaining case: YM3*)


156 
by (expand_case_tac "K = ?y" 1);


157 
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));


158 
(*...we assume X is a recent message and handle this case by contradiction*)


159 
by (blast_tac (claset() addSEs knows_Spy_partsEs


160 
delrules [conjI] (*no splitup to 4 subgoals*)) 1);


161 
val lemma = result();


162 


163 
Goal "[ Says Server A \


164 
\ {Crypt (shrK A) {Agent B, Key K, na, nb}, X} : set evs; \


165 
\ Says Server A' \


166 
\ {Crypt (shrK A') {Agent B', Key K, na', nb'}, X'} : set evs; \


167 
\ evs : yahalom ] \


168 
\ ==> A=A' & B=B' & na=na' & nb=nb'";


169 
by (prove_unique_tac lemma 1);


170 
qed "unique_session_keys";


171 


172 


173 
(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)


174 


175 
Goal "[ A ~: bad; B ~: bad; evs : yahalom ] \


176 
\ ==> Says Server A \


177 
\ {Crypt (shrK A) {Agent B, Key K, na, nb}, \


178 
\ Crypt (shrK B) {Agent A, Key K}} \


179 
\ : set evs > \


180 
\ Key K ~: analz (knows Spy evs)";


181 
by (etac yahalom.induct 1);


182 
by analz_knows_Spy_tac;


183 
by (ALLGOALS


184 
(asm_simp_tac


185 
(simpset() addsimps split_ifs @ pushes @


186 
[analz_insert_eq, analz_insert_freshK])));


187 
(*YM3*)


188 
by (blast_tac (claset() delrules [impCE]


189 
addSEs knows_Spy_partsEs


190 
addIs [impOfSubs analz_subset_parts]) 2);


191 
(*Fake*)


192 
by (spy_analz_tac 1);


193 
val lemma = result() RS mp RSN(2,rev_notE);


194 


195 


196 
(*Final version*)


197 
Goal "[ Says Server A \


198 
\ {Crypt (shrK A) {Agent B, Key K, na, nb}, \


199 
\ Crypt (shrK B) {Agent A, Key K}} \


200 
\ : set evs; \


201 
\ A ~: bad; B ~: bad; evs : yahalom ] \


202 
\ ==> Key K ~: analz (knows Spy evs)";


203 
by (blast_tac (claset() addSEs [lemma]) 1);


204 
qed "Spy_not_see_encrypted_key";


205 


206 


207 
(** Security Guarantee for A upon receiving YM3 **)


208 


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


210 
Goal "[ Crypt (shrK A) {Agent B, Key K, na, nb} : parts (knows Spy evs); \


211 
\ A ~: bad; evs : yahalom ] \


212 
\ ==> Says Server A \


213 
\ {Crypt (shrK A) {Agent B, Key K, na, nb}, \


214 
\ Crypt (shrK B) {Agent A, Key K}} \


215 
\ : set evs";


216 
by (etac rev_mp 1);


217 
by (parts_induct_tac 1);


218 
by (Fake_parts_insert_tac 1);


219 
qed "A_trusts_YM3";


220 


221 
(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)


222 
Goal "[ Crypt (shrK A) {Agent B, Key K, na, nb} : parts (knows Spy evs); \


223 
\ A ~: bad; B ~: bad; evs : yahalom ] \


224 
\ ==> Key K ~: analz (knows Spy evs)";


225 
by (blast_tac (claset() addSDs [A_trusts_YM3, Spy_not_see_encrypted_key]) 1);


226 
qed "A_gets_good_key";


227 


228 
(** Security Guarantees for B upon receiving YM4 **)


229 


230 
(*B knows, by the first part of A's message, that the Server distributed


231 
the key for A and B. But this part says nothing about nonces.*)


232 
Goal "[ Crypt (shrK B) {Agent A, Key K} : parts (knows Spy evs); \


233 
\ B ~: bad; evs : yahalom ] \


234 
\ ==> EX NA NB. Says Server A \


235 
\ {Crypt (shrK A) {Agent B, Key K, \


236 
\ Nonce NA, Nonce NB}, \


237 
\ Crypt (shrK B) {Agent A, Key K}} \


238 
\ : set evs";


239 
by (etac rev_mp 1);


240 
by (parts_induct_tac 1);


241 
by (Fake_parts_insert_tac 1);


242 
(*YM3*)


243 
by (Blast_tac 1);


244 
qed "B_trusts_YM4_shrK";


245 


246 
(** Up to now, the reasoning is similar to standard Yahalom. Now the


247 
doubtful reasoning occurs. We should not be assuming that an unknown


248 
key is secure, but the model allows us to: there is no Oops rule to


249 
let session keys go.*)


250 


251 
(*B knows, by the second part of A's message, that the Server distributed


252 
the key quoting nonce NB. This part says nothing about agent names.


253 
Secrecy of K is assumed; the valid Yahalom proof uses (and later proves)


254 
the secrecy of NB.*)


255 
Goal "evs : yahalom \


256 
\ ==> Key K ~: analz (knows Spy evs) > \


257 
\ Crypt K (Nonce NB) : parts (knows Spy evs) > \


258 
\ (EX A B NA. Says Server A \


259 
\ {Crypt (shrK A) {Agent B, Key K, \


260 
\ Nonce NA, Nonce NB}, \


261 
\ Crypt (shrK B) {Agent A, Key K}} \


262 
\ : set evs)";


263 
by (parts_induct_tac 1);


264 
by (ALLGOALS Clarify_tac);


265 
(*YM3 & Fake*)


266 
by (Blast_tac 2);


267 
by (Fake_parts_insert_tac 1);


268 
(*YM4*)


269 
(*A is uncompromised because NB is secure*)


270 
by (g_not_bad_tac "A" 1);


271 
(*A's certificate guarantees the existence of the Server message*)


272 
by (blast_tac (claset() addDs [Says_imp_knows_Spy RS parts.Inj RS parts.Fst RS


273 
A_trusts_YM3]) 1);


274 
bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp));


275 


276 


277 
(*B's session key guarantee from YM4. The two certificates contribute to a


278 
single conclusion about the Server's message. *)


279 
Goal "[ Gets B {Crypt (shrK B) {Agent A, Key K}, \


280 
\ Crypt K (Nonce NB)} : set evs; \


281 
\ Says B Server \


282 
\ {Agent B, Nonce NB, Crypt (shrK B) {Agent A, Nonce NA}} \


283 
\ : set evs; \


284 
\ A ~: bad; B ~: bad; evs : yahalom ] \


285 
\ ==> EX na nb. Says Server A \


286 
\ {Crypt (shrK A) {Agent B, Key K, na, nb}, \


287 
\ Crypt (shrK B) {Agent A, Key K}} \


288 
\ : set evs";


289 
by (etac (Gets_imp_knows_Spy RS parts.Inj RS MPair_parts) 1 THEN


290 
assume_tac 1 THEN dtac B_trusts_YM4_shrK 1);


291 
by (dtac B_trusts_YM4_newK 3);


292 
by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));


293 
by (etac Spy_not_see_encrypted_key 1 THEN REPEAT (assume_tac 1));

7499

294 
by (ftac unique_session_keys 1 THEN REPEAT (assume_tac 1));

6400

295 
by (blast_tac (claset() addDs []) 1);


296 
qed "B_trusts_YM4";


297 


298 


299 
(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)


300 
Goal "[ Gets B {Crypt (shrK B) {Agent A, Key K}, \


301 
\ Crypt K (Nonce NB)} : set evs; \


302 
\ Says B Server \


303 
\ {Agent B, Nonce NB, Crypt (shrK B) {Agent A, Nonce NA}} \


304 
\ : set evs; \


305 
\ A ~: bad; B ~: bad; evs : yahalom ] \


306 
\ ==> Key K ~: analz (knows Spy evs)";


307 
by (blast_tac (claset() addSDs [B_trusts_YM4, Spy_not_see_encrypted_key]) 1);


308 
qed "B_gets_good_key";


309 


310 


311 
(*** Authenticating B to A: these proofs are not considered.


312 
They are irrelevant to showing the need for Oops. ***)


313 


314 


315 
(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)


316 


317 
(*Assuming the session key is secure, if both certificates are present then


318 
A has said NB. We can't be sure about the rest of A's message, but only


319 
NB matters for freshness.*)


320 
Goal "evs : yahalom \


321 
\ ==> Key K ~: analz (knows Spy evs) > \


322 
\ Crypt K (Nonce NB) : parts (knows Spy evs) > \


323 
\ Crypt (shrK B) {Agent A, Key K} : parts (knows Spy evs) > \


324 
\ B ~: bad > \


325 
\ (EX X. Says A B {X, Crypt K (Nonce NB)} : set evs)";


326 
by (parts_induct_tac 1);


327 
(*Fake*)


328 
by (Fake_parts_insert_tac 1);


329 
(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)


330 
by (fast_tac (claset() addSDs [Crypt_imp_keysFor] addss (simpset())) 1);


331 
(*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*)


332 
by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);


333 
(*yes: apply unicity of session keys*)


334 
by (g_not_bad_tac "Aa" 1);


335 
by (blast_tac (claset() addSEs [MPair_parts]


336 
addSDs [A_trusts_YM3, B_trusts_YM4_shrK]


337 
addDs [Says_imp_knows_Spy RS parts.Inj,


338 
unique_session_keys]) 1);


339 
qed_spec_mp "A_Said_YM3_lemma";


340 


341 
(*If B receives YM4 then A has used nonce NB (and therefore is alive).


342 
Moreover, A associates K with NB (thus is talking about the same run).


343 
Other premises guarantee secrecy of K.*)


344 
Goal "[ Gets B {Crypt (shrK B) {Agent A, Key K}, \


345 
\ Crypt K (Nonce NB)} : set evs; \


346 
\ Says B Server \


347 
\ {Agent B, Nonce NB, Crypt (shrK B) {Agent A, Nonce NA}} \


348 
\ : set evs; \


349 
\ A ~: bad; B ~: bad; evs : yahalom ] \


350 
\ ==> EX X. Says A B {X, Crypt K (Nonce NB)} : set evs";

7499

351 
by (ftac B_trusts_YM4 1);

6400

352 
by (REPEAT_FIRST assume_tac);


353 
by (etac (Gets_imp_knows_Spy RS parts.Inj RS MPair_parts) 1 THEN assume_tac 1);


354 
by (Clarify_tac 1);


355 
by (rtac A_Said_YM3_lemma 1);


356 
by (rtac Spy_not_see_encrypted_key 2);


357 
by (REPEAT_FIRST assume_tac);


358 
qed_spec_mp "YM4_imp_A_Said_YM3";
