# HG changeset patch # User paulson # Date 987072305 -7200 # Node ID a6816d47f41db00a5b5836dd52d2a0ed2f192609 # Parent c8bbf4c4bc2da310927a903c284cf32ff7746d0c converted many HOL/Auth theories to Isar scripts diff -r c8bbf4c4bc2d -r a6816d47f41d src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Wed Apr 11 11:53:54 2001 +0200 +++ b/src/HOL/Auth/Message.thy Thu Apr 12 12:45:05 2001 +0200 @@ -135,6 +135,8 @@ use "Message_lemmas.ML" +lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard] + lemma Fake_parts_insert_in_Un: "[|Z \ parts (insert X H); X: synth (analz H)|] ==> Z \ synth (analz H) \ parts H"; diff -r c8bbf4c4bc2d -r a6816d47f41d src/HOL/Auth/Message_lemmas.ML --- a/src/HOL/Auth/Message_lemmas.ML Wed Apr 11 11:53:54 2001 +0200 +++ b/src/HOL/Auth/Message_lemmas.ML Thu Apr 12 12:45:05 2001 +0200 @@ -50,7 +50,7 @@ by Auto_tac; qed "Friend_image_eq"; -Goal "(Key x \\ Key`A) = (x:A)"; +Goal "(Key x \\ Key`A) = (x\\A)"; by Auto_tac; qed "Key_image_eq"; @@ -82,12 +82,12 @@ by (Blast_tac 1); qed "keysFor_Un"; -Goalw [keysFor_def] "keysFor (UN i:A. H i) = (UN i:A. keysFor (H i))"; +Goalw [keysFor_def] "keysFor (\\i\\A. H i) = (\\i\\A. keysFor (H i))"; by (Blast_tac 1); qed "keysFor_UN"; (*Monotonicity*) -Goalw [keysFor_def] "G<=H ==> keysFor(G) <= keysFor(H)"; +Goalw [keysFor_def] "G\\H ==> keysFor(G) \\ keysFor(H)"; by (Blast_tac 1); qed "keysFor_mono"; @@ -154,7 +154,7 @@ MPair_parts is left as SAFE because it speeds up proofs. The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*) -Goal "H <= parts(H)"; +Goal "H \\ parts(H)"; by (Blast_tac 1); qed "parts_increasing"; @@ -167,13 +167,13 @@ qed "parts_empty"; Addsimps [parts_empty]; -Goal "X: parts{} ==> P"; +Goal "X\\ parts{} ==> P"; by (Asm_full_simp_tac 1); qed "parts_emptyE"; AddSEs [parts_emptyE]; (*WARNING: loops if H = {Y}, therefore must not be repeated!*) -Goal "X: parts H ==> EX Y:H. X: parts {Y}"; +Goal "X\\ parts H ==> \\Y\\H. X\\ parts {Y}"; by (etac parts.induct 1); by (ALLGOALS Blast_tac); qed "parts_singleton"; @@ -181,11 +181,11 @@ (** Unions **) -Goal "parts(G) Un parts(H) <= parts(G Un H)"; +Goal "parts(G) Un parts(H) \\ parts(G Un H)"; by (REPEAT (ares_tac [Un_least, parts_mono, Un_upper1, Un_upper2] 1)); val parts_Un_subset1 = result(); -Goal "parts(G Un H) <= parts(G) Un parts(H)"; +Goal "parts(G Un H) \\ parts(G) Un parts(H)"; by (rtac subsetI 1); by (etac parts.induct 1); by (ALLGOALS Blast_tac); @@ -207,17 +207,17 @@ by (simp_tac (simpset() addsimps [parts_insert RS sym]) 1); qed "parts_insert2"; -Goal "(UN x:A. parts(H x)) <= parts(UN x:A. H x)"; +Goal "(\\x\\A. parts(H x)) \\ parts(\\x\\A. H x)"; by (REPEAT (ares_tac [UN_least, parts_mono, UN_upper] 1)); val parts_UN_subset1 = result(); -Goal "parts(UN x:A. H x) <= (UN x:A. parts(H x))"; +Goal "parts(\\x\\A. H x) \\ (\\x\\A. parts(H x))"; by (rtac subsetI 1); by (etac parts.induct 1); by (ALLGOALS Blast_tac); val parts_UN_subset2 = result(); -Goal "parts(UN x:A. H x) = (UN x:A. parts(H x))"; +Goal "parts(\\x\\A. H x) = (\\x\\A. parts(H x))"; by (REPEAT (ares_tac [equalityI, parts_UN_subset1, parts_UN_subset2] 1)); qed "parts_UN"; @@ -227,13 +227,13 @@ AddSEs [parts_Un RS equalityD1 RS subsetD RS UnE, parts_UN RS equalityD1 RS subsetD RS UN_E]; -Goal "insert X (parts H) <= parts(insert X H)"; +Goal "insert X (parts H) \\ parts(insert X H)"; by (blast_tac (claset() addIs [impOfSubs parts_mono]) 1); qed "parts_insert_subset"; (** Idempotence and transitivity **) -Goal "X: parts (parts H) ==> X: parts H"; +Goal "X\\ parts (parts H) ==> X\\ parts H"; by (etac parts.induct 1); by (ALLGOALS Blast_tac); qed "parts_partsD"; @@ -244,19 +244,19 @@ qed "parts_idem"; Addsimps [parts_idem]; -Goal "[| X: parts G; G <= parts H |] ==> X: parts H"; +Goal "[| X\\ parts G; G \\ parts H |] ==> X\\ parts H"; by (dtac parts_mono 1); by (Blast_tac 1); qed "parts_trans"; (*Cut*) -Goal "[| Y: parts (insert X G); X: parts H |] \ -\ ==> Y: parts (G Un H)"; +Goal "[| Y\\ parts (insert X G); X\\ parts H |] \ +\ ==> Y\\ parts (G Un H)"; by (etac parts_trans 1); by Auto_tac; qed "parts_cut"; -Goal "X: parts H ==> parts (insert X H) = parts H"; +Goal "X\\ parts H ==> parts (insert X H) = parts H"; by (fast_tac (claset() addSDs [parts_cut] addIs [parts_insertI] addss (simpset())) 1); @@ -326,7 +326,7 @@ (*In any message, there is an upper bound N on its greatest nonce.*) -Goal "EX N. ALL n. N<=n --> Nonce n \\ parts {msg}"; +Goal "\\N. \\n. N\\n --> Nonce n \\ parts {msg}"; by (induct_tac "msg" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [exI, parts_insert2]))); (*MPair case: blast_tac works out the necessary sum itself!*) @@ -350,11 +350,11 @@ AddSEs [MPair_analz]; (*Making it safe speeds up proofs*) -Goal "H <= analz(H)"; +Goal "H \\ analz(H)"; by (Blast_tac 1); qed "analz_increasing"; -Goal "analz H <= parts H"; +Goal "analz H \\ parts H"; by (rtac subsetI 1); by (etac analz.induct 1); by (ALLGOALS Blast_tac); @@ -391,11 +391,11 @@ (*Converse fails: we can analz more from the union than from the separate parts, as a key in one might decrypt a message in the other*) -Goal "analz(G) Un analz(H) <= analz(G Un H)"; +Goal "analz(G) Un analz(H) \\ analz(G Un H)"; by (REPEAT (ares_tac [Un_least, analz_mono, Un_upper1, Un_upper2] 1)); qed "analz_Un"; -Goal "insert X (analz H) <= analz(insert X H)"; +Goal "insert X (analz H) \\ analz(insert X H)"; by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1); qed "analz_insert"; @@ -447,7 +447,7 @@ qed "analz_insert_Crypt"; Goal "Key (invKey K) \\ analz H ==> \ -\ analz (insert (Crypt K X) H) <= \ +\ analz (insert (Crypt K X) H) \\ \ \ insert (Crypt K X) (analz (insert X H))"; by (rtac subsetI 1); by (eres_inst_tac [("xa","x")] analz.induct 1); @@ -455,7 +455,7 @@ val lemma1 = result(); Goal "Key (invKey K) \\ analz H ==> \ -\ insert (Crypt K X) (analz (insert X H)) <= \ +\ insert (Crypt K X) (analz (insert X H)) \\ \ \ analz (insert (Crypt K X) H)"; by Auto_tac; by (eres_inst_tac [("xa","x")] analz.induct 1); @@ -487,7 +487,7 @@ analz_insert_Hash, analz_insert_MPair, analz_Crypt_if]; (*This rule supposes "for the sake of argument" that we have the key.*) -Goal "analz (insert (Crypt K X) H) <= \ +Goal "analz (insert (Crypt K X) H) \\ \ \ insert (Crypt K X) (analz (insert X H))"; by (rtac subsetI 1); by (etac analz.induct 1); @@ -506,7 +506,7 @@ (** Idempotence and transitivity **) -Goal "X: analz (analz H) ==> X: analz H"; +Goal "X\\ analz (analz H) ==> X\\ analz H"; by (etac analz.induct 1); by (ALLGOALS Blast_tac); qed "analz_analzD"; @@ -517,13 +517,13 @@ qed "analz_idem"; Addsimps [analz_idem]; -Goal "[| X: analz G; G <= analz H |] ==> X: analz H"; +Goal "[| X\\ analz G; G \\ analz H |] ==> X\\ analz H"; by (dtac analz_mono 1); by (Blast_tac 1); qed "analz_trans"; (*Cut; Lemma 2 of Lowe*) -Goal "[| Y: analz (insert X H); X: analz H |] ==> Y: analz H"; +Goal "[| Y\\ analz (insert X H); X\\ analz H |] ==> Y\\ analz H"; by (etac analz_trans 1); by (Blast_tac 1); qed "analz_cut"; @@ -535,15 +535,15 @@ (*This rewrite rule helps in the simplification of messages that involve the forwarding of unknown components (X). Without it, removing occurrences of X can be very complicated. *) -Goal "X: analz H ==> analz (insert X H) = analz H"; +Goal "X\\ analz H ==> analz (insert X H) = analz H"; by (blast_tac (claset() addIs [analz_cut, analz_insertI]) 1); qed "analz_insert_eq"; (** A congruence rule for "analz" **) -Goal "[| analz G <= analz G'; analz H <= analz H' \ -\ |] ==> analz (G Un H) <= analz (G' Un H')"; +Goal "[| analz G \\ analz G'; analz H \\ analz H' \ +\ |] ==> analz (G Un H) \\ analz (G' Un H')"; by (Clarify_tac 1); by (etac analz.induct 1); by (ALLGOALS (best_tac (claset() addIs [analz_mono RS subsetD]))); @@ -562,20 +562,19 @@ qed "analz_insert_cong"; (*If there are no pairs or encryptions then analz does nothing*) -Goal "[| ALL X Y. {|X,Y|} \\ H; ALL X K. Crypt K X \\ H |] ==> \ -\ analz H = H"; +Goal "[| \\X Y. {|X,Y|} \\ H; \\X K. Crypt K X \\ H |] ==> analz H = H"; by Safe_tac; by (etac analz.induct 1); by (ALLGOALS Blast_tac); qed "analz_trivial"; (*These two are obsolete (with a single Spy) but cost little to prove...*) -Goal "X: analz (UN i:A. analz (H i)) ==> X: analz (UN i:A. H i)"; +Goal "X\\ analz (\\i\\A. analz (H i)) ==> X\\ analz (\\i\\A. H i)"; by (etac analz.induct 1); by (ALLGOALS (blast_tac (claset() addIs [impOfSubs analz_mono]))); val lemma = result(); -Goal "analz (UN i:A. analz (H i)) = analz (UN i:A. H i)"; +Goal "analz (\\i\\A. analz (H i)) = analz (\\i\\A. H i)"; by (blast_tac (claset() addIs [lemma, impOfSubs analz_mono]) 1); qed "analz_UN_analz"; Addsimps [analz_UN_analz]; @@ -583,7 +582,7 @@ (**** Inductive relation "synth" ****) -Goal "H <= synth(H)"; +Goal "H \\ synth(H)"; by (Blast_tac 1); qed "synth_increasing"; @@ -591,17 +590,17 @@ (*Converse fails: we can synth more from the union than from the separate parts, building a compound message using elements of each.*) -Goal "synth(G) Un synth(H) <= synth(G Un H)"; +Goal "synth(G) Un synth(H) \\ synth(G Un H)"; by (REPEAT (ares_tac [Un_least, synth_mono, Un_upper1, Un_upper2] 1)); qed "synth_Un"; -Goal "insert X (synth H) <= synth(insert X H)"; +Goal "insert X (synth H) \\ synth(insert X H)"; by (blast_tac (claset() addIs [impOfSubs synth_mono]) 1); qed "synth_insert"; (** Idempotence and transitivity **) -Goal "X: synth (synth H) ==> X: synth H"; +Goal "X\\ synth (synth H) ==> X\\ synth H"; by (etac synth.induct 1); by (ALLGOALS Blast_tac); qed "synth_synthD"; @@ -611,13 +610,13 @@ by (Blast_tac 1); qed "synth_idem"; -Goal "[| X: synth G; G <= synth H |] ==> X: synth H"; +Goal "[| X\\ synth G; G \\ synth H |] ==> X\\ synth H"; by (dtac synth_mono 1); by (Blast_tac 1); qed "synth_trans"; (*Cut; Lemma 2 of Lowe*) -Goal "[| Y: synth (insert X H); X: synth H |] ==> Y: synth H"; +Goal "[| Y\\ synth (insert X H); X\\ synth H |] ==> Y\\ synth H"; by (etac synth_trans 1); by (Blast_tac 1); qed "synth_cut"; @@ -688,23 +687,23 @@ (** For reasoning about the Fake rule in traces **) -Goal "X: G ==> parts(insert X H) <= parts G Un parts H"; +Goal "X\\ G ==> parts(insert X H) \\ parts G Un parts H"; by (rtac ([parts_mono, parts_Un_subset2] MRS subset_trans) 1); by (Blast_tac 1); qed "parts_insert_subset_Un"; (*More specifically for Fake. Very occasionally we could do with a version - of the form parts{X} <= synth (analz H) Un parts H *) -Goal "X: synth (analz H) ==> \ -\ parts (insert X H) <= synth (analz H) Un parts H"; + of the form parts{X} \\ synth (analz H) Un parts H *) +Goal "X\\ synth (analz H) ==> \ +\ parts (insert X H) \\ synth (analz H) Un parts H"; by (dtac parts_insert_subset_Un 1); by (Full_simp_tac 1); by (Blast_tac 1); qed "Fake_parts_insert"; (*H is sometimes (Key ` KK Un spies evs), so can't put G=H*) -Goal "X: synth (analz G) ==> \ -\ analz (insert X H) <= synth (analz G) Un analz (G Un H)"; +Goal "X\\ synth (analz G) ==> \ +\ analz (insert X H) \\ synth (analz G) Un analz (G Un H)"; by (rtac subsetI 1); by (subgoal_tac "x \\ analz (synth (analz G) Un H)" 1); by (blast_tac (claset() addIs [impOfSubs analz_mono, @@ -713,11 +712,11 @@ by (Blast_tac 1); qed "Fake_analz_insert"; -Goal "(X: analz H & X: parts H) = (X: analz H)"; +Goal "(X\\ analz H & X\\ parts H) = (X\\ analz H)"; by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1); val analz_conj_parts = result(); -Goal "(X: analz H | X: parts H) = (X: parts H)"; +Goal "(X\\ analz H | X\\ parts H) = (X\\ parts H)"; by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1); val analz_disj_parts = result(); diff -r c8bbf4c4bc2d -r a6816d47f41d src/HOL/Auth/NS_Shared.thy --- a/src/HOL/Auth/NS_Shared.thy Wed Apr 11 11:53:54 2001 +0200 +++ b/src/HOL/Auth/NS_Shared.thy Thu Apr 12 12:45:05 2001 +0200 @@ -20,8 +20,8 @@ (*The spy MAY say anything he CAN say. We do not expect him to invent new nonces here, but he can also use NS1. Common to all similar protocols.*) - Fake: "\evs \ ns_shared; X \ synth (analz (spies evs))\ - \ Says Spy B X # evs \ ns_shared" + Fake: "\evsf \ ns_shared; X \ synth (analz (spies evsf))\ + \ Says Spy B X # evsf \ ns_shared" (*Alice initiates a protocol run, requesting to talk to any B*) NS1: "\evs1 \ ns_shared; Nonce NA \ used evs1\ @@ -74,10 +74,8 @@ declare Says_imp_knows_Spy [THEN parts.Inj, dest] declare parts.Body [dest] -declare MPair_parts [elim!] (*can speed up some proofs*) - -declare analz_subset_parts [THEN subsetD, dest] -declare Fake_parts_insert [THEN subsetD, dest] +declare Fake_parts_insert_in_Un [dest] +declare analz_into_parts [dest] declare image_eq_UN [simp] (*accelerates proofs involving nested images*) @@ -123,7 +121,6 @@ apply blast+; done - lemma Spy_analz_shrK [simp]: "evs \ ns_shared \ (Key (shrK A) \ analz (spies evs)) = (A \ bad)" by auto @@ -310,8 +307,7 @@ Crypt K (Nonce NB) \ parts (spies evs) \ Says B A (Crypt K (Nonce NB)) \ set evs" apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies) -apply analz_mono_contra -apply simp_all +apply (analz_mono_contra, simp_all) apply blast (*Fake*) (*NS2: contradiction from the assumptions Key K \ used evs2 and Crypt K (Nonce NB) \ parts (spies evs2) *) diff -r c8bbf4c4bc2d -r a6816d47f41d src/HOL/Auth/OtwayRees.ML --- a/src/HOL/Auth/OtwayRees.ML Wed Apr 11 11:53:54 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,411 +0,0 @@ -(* Title: HOL/Auth/OtwayRees - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1996 University of Cambridge - -Inductive relation "otway" for the Otway-Rees protocol. - -Version that encrypts Nonce NB - -From page 244 of - Burrows, Abadi and Needham. A Logic of Authentication. - Proc. Royal Soc. 426 (1989) -*) - -AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body]; -AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; - - -(*A "possibility property": there are traces that reach the end*) -Goal "B \\ Server \ -\ ==> \\K. \\evs \\ otway. \ -\ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \ -\ \\ set evs"; -by (REPEAT (resolve_tac [exI,bexI] 1)); -by (rtac (otway.Nil RS - otway.OR1 RS otway.Reception RS - otway.OR2 RS otway.Reception RS - otway.OR3 RS otway.Reception RS otway.OR4) 2); -by possibility_tac; -result(); - -Goal "[| Gets B X \\ set evs; evs \\ otway |] ==> \\A. Says A B X \\ set evs"; -by (etac rev_mp 1); -by (etac otway.induct 1); -by Auto_tac; -qed"Gets_imp_Says"; - -(*Must be proved separately for each protocol*) -Goal "[| Gets B X \\ set evs; evs \\ otway |] ==> X \\ knows Spy evs"; -by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1); -qed"Gets_imp_knows_Spy"; -AddSDs [Gets_imp_knows_Spy RS parts.Inj]; - - -(**** Inductive proofs about otway ****) - -(** For reasoning about the encrypted portion of messages **) - -Goal "[| Gets B {|N, Agent A, Agent B, X|} \\ set evs; evs \\ otway |] \ -\ ==> X \\ analz (knows Spy evs)"; -by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1); -qed "OR2_analz_knows_Spy"; - -Goal "[| Gets B {|N, X, Crypt (shrK B) X'|} \\ set evs; evs \\ otway |] \ -\ ==> X \\ analz (knows Spy evs)"; -by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1); -qed "OR4_analz_knows_Spy"; - -Goal "Says Server B {|NA, X, Crypt K' {|NB,K|}|} \\ set evs \ -\ ==> K \\ parts (knows Spy evs)"; -by (Blast_tac 1); -qed "Oops_parts_knows_Spy"; - -bind_thm ("OR2_parts_knows_Spy", - OR2_analz_knows_Spy RS (impOfSubs analz_subset_parts)); -bind_thm ("OR4_parts_knows_Spy", - OR4_analz_knows_Spy RS (impOfSubs analz_subset_parts)); - -(*For proving the easier theorems about X \\ parts (knows Spy evs).*) -fun parts_induct_tac i = - etac otway.induct i THEN - ftac Oops_parts_knows_Spy (i+7) THEN - ftac OR4_parts_knows_Spy (i+6) THEN - ftac OR2_parts_knows_Spy (i+4) THEN - prove_simple_subgoals_tac i; - - -(** Theorems of the form X \\ parts (knows Spy evs) imply that NOBODY - sends messages containing X! **) - -(*Spy never sees a good agent's shared key!*) -Goal "evs \\ otway ==> (Key (shrK A) \\ parts (knows Spy evs)) = (A \\ bad)"; -by (parts_induct_tac 1); -by (ALLGOALS Blast_tac); -qed "Spy_see_shrK"; -Addsimps [Spy_see_shrK]; - -Goal "evs \\ otway ==> (Key (shrK A) \\ analz (knows Spy evs)) = (A \\ bad)"; -by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); -qed "Spy_analz_shrK"; -Addsimps [Spy_analz_shrK]; - -AddSDs [Spy_see_shrK RSN (2, rev_iffD1), - Spy_analz_shrK RSN (2, rev_iffD1)]; - - -(*** Proofs involving analz ***) - -(*Describes the form of K and NA when the Server sends this message. Also - for Oops case.*) -Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \\ set evs; \ -\ evs \\ otway |] \ -\ ==> K \\ range shrK & (\\i. NA = Nonce i) & (\\j. NB = Nonce j)"; -by (etac rev_mp 1); -by (etac otway.induct 1); -by (ALLGOALS Simp_tac); -by (ALLGOALS Blast_tac); -qed "Says_Server_message_form"; - - -(*For proofs involving analz.*) -val analz_knows_Spy_tac = - dtac OR2_analz_knows_Spy 5 THEN assume_tac 5 THEN - dtac OR4_analz_knows_Spy 7 THEN assume_tac 7 THEN - ftac Says_Server_message_form 8 THEN assume_tac 8 THEN - REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 8); - - -(**** - The following is to prove theorems of the form - - Key K \\ analz (insert (Key KAB) (knows Spy evs)) ==> - Key K \\ analz (knows Spy evs) - - A more general formula must be proved inductively. -****) - - -(** Session keys are not used to encrypt other session keys **) - -(*The equality makes the induction hypothesis easier to apply*) -Goal "evs \\ otway ==> ALL K KK. KK <= - (range shrK) --> \ -\ (Key K \\ analz (Key`KK Un (knows Spy evs))) = \ -\ (K \\ KK | Key K \\ analz (knows Spy evs))"; -by (etac otway.induct 1); -by analz_knows_Spy_tac; -by (REPEAT_FIRST (resolve_tac [allI, impI])); -by (REPEAT_FIRST (rtac analz_image_freshK_lemma)); -by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); -(*Fake*) -by (spy_analz_tac 1); -qed_spec_mp "analz_image_freshK"; - - -Goal "[| evs \\ otway; KAB \\ range shrK |] \ -\ ==> Key K \\ analz (insert (Key KAB) (knows Spy evs)) = \ -\ (K = KAB | Key K \\ analz (knows Spy evs))"; -by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); -qed "analz_insert_freshK"; - - -(*** The Key K uniquely identifies the Server's message. **) - -Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \\ set evs; \ -\ Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \\ set evs; \ -\ evs \\ otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'"; -by (etac rev_mp 1); -by (etac rev_mp 1); -by (etac otway.induct 1); -by (ALLGOALS Asm_simp_tac); -(*Remaining cases: OR3 and OR4*) -by (REPEAT (Blast_tac 1)); -qed "unique_session_keys"; - - -(**** Authenticity properties relating to NA ****) - -(*Only OR1 can have caused such a part of a message to appear.*) -Goal "[| A \\ bad; evs \\ otway |] \ -\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \\ parts (knows Spy evs) --> \ -\ Says A B {|NA, Agent A, Agent B, \ -\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ -\ \\ set evs"; -by (parts_induct_tac 1); -by (Blast_tac 1); -qed_spec_mp "Crypt_imp_OR1"; - -Goal "[| Gets B {|NA, Agent A, Agent B, \ -\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\ set evs; \ -\ A \\ bad; evs \\ otway |] \ -\ ==> Says A B {|NA, Agent A, Agent B, \ -\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ -\ \\ set evs"; -by (blast_tac (claset() addDs [Crypt_imp_OR1]) 1); -qed"Crypt_imp_OR1_Gets"; - - -(** The Nonce NA uniquely identifies A's message. **) - -Goal "[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (knows Spy evs); \ -\ Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (knows Spy evs); \ -\ evs \\ otway; A \\ bad |] \ -\ ==> B = C"; -by (etac rev_mp 1); -by (etac rev_mp 1); -by (parts_induct_tac 1); -(*Fake, OR1*) -by (REPEAT (Blast_tac 1)); -qed "unique_NA"; - - -(*It is impossible to re-use a nonce in both OR1 and OR2. This holds because - OR2 encrypts Nonce NB. It prevents the attack that can occur in the - over-simplified version of this protocol: see OtwayRees_Bad.*) -Goal "[| A \\ bad; evs \\ otway |] \ -\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \\ parts (knows Spy evs) --> \ -\ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \ -\ \\ parts (knows Spy evs)"; -by (parts_induct_tac 1); -by Auto_tac; -qed_spec_mp "no_nonce_OR1_OR2"; - -val nonce_OR1_OR2_E = no_nonce_OR1_OR2 RSN (2, rev_notE); - -(*Crucial property: If the encrypted message appears, and A has used NA - to start a run, then it originated with the Server!*) -Goal "[| A \\ bad; evs \\ otway |] \ -\ ==> Says A B {|NA, Agent A, Agent B, \ -\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\ set evs --> \ -\ Crypt (shrK A) {|NA, Key K|} \\ parts (knows Spy evs) \ -\ --> (\\NB. Says Server B \ -\ {|NA, \ -\ Crypt (shrK A) {|NA, Key K|}, \ -\ Crypt (shrK B) {|NB, Key K|}|} \\ set evs)"; -by (parts_induct_tac 1); -by (Blast_tac 1); -(*OR1: it cannot be a new Nonce, contradiction.*) -by (Blast_tac 1); -(*OR4*) -by (blast_tac (claset() addSIs [Crypt_imp_OR1]) 2); -by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1); -by (blast_tac (claset() addSEs [nonce_OR1_OR2_E] addIs [unique_NA]) 1); -qed_spec_mp "NA_Crypt_imp_Server_msg"; - - -(*Corollary: if A receives B's OR4 message and the nonce NA agrees - then the key really did come from the Server! CANNOT prove this of the - bad form of this protocol, even though we can prove - Spy_not_see_encrypted_key*) -Goal "[| Says A B {|NA, Agent A, Agent B, \ -\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\ set evs; \ -\ Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} \\ set evs; \ -\ A \\ bad; evs \\ otway |] \ -\ ==> \\NB. Says Server B \ -\ {|NA, \ -\ Crypt (shrK A) {|NA, Key K|}, \ -\ Crypt (shrK B) {|NB, Key K|}|} \ -\ \\ set evs"; -by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1); -qed "A_trusts_OR4"; - - -(** Crucial secrecy property: Spy does not see the keys sent in msg OR3 - Does not in itself guarantee security: an attack could violate - the premises, e.g. by having A=Spy **) - -Goal "[| A \\ bad; B \\ bad; evs \\ otway |] \ -\ ==> Says Server B \ -\ {|NA, Crypt (shrK A) {|NA, Key K|}, \ -\ Crypt (shrK B) {|NB, Key K|}|} \\ set evs --> \ -\ Notes Spy {|NA, NB, Key K|} \\ set evs --> \ -\ Key K \\ analz (knows Spy evs)"; -by (etac otway.induct 1); -by analz_knows_Spy_tac; -by (ALLGOALS - (asm_simp_tac (simpset() addcongs [conj_cong] - addsimps [analz_insert_eq, analz_insert_freshK] - @ pushes @ split_ifs))); -(*Oops*) -by (blast_tac (claset() addSDs [unique_session_keys]) 4); -(*OR4*) -by (Blast_tac 3); -(*OR3*) -by (Blast_tac 2); -(*Fake*) -by (spy_analz_tac 1); -val lemma = result() RS mp RS mp RSN(2,rev_notE); - -Goal "[| Says Server B \ -\ {|NA, Crypt (shrK A) {|NA, Key K|}, \ -\ Crypt (shrK B) {|NB, Key K|}|} \\ set evs; \ -\ Notes Spy {|NA, NB, Key K|} \\ set evs; \ -\ A \\ bad; B \\ bad; evs \\ otway |] \ -\ ==> Key K \\ analz (knows Spy evs)"; -by (blast_tac (claset() addDs [Says_Server_message_form] addSEs [lemma]) 1); -qed "Spy_not_see_encrypted_key"; - - -(*A's guarantee. The Oops premise quantifies over NB because A cannot know - what it is.*) -Goal "[| Says A B {|NA, Agent A, Agent B, \ -\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\ set evs; \ -\ Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} \\ set evs; \ -\ ALL NB. Notes Spy {|NA, NB, Key K|} \\ set evs; \ -\ A \\ bad; B \\ bad; evs \\ otway |] \ -\ ==> Key K \\ analz (knows Spy evs)"; -by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1); -qed "A_gets_good_key"; - - -(**** Authenticity properties relating to NB ****) - -(*Only OR2 can have caused such a part of a message to appear. We do not - know anything about X: it does NOT have to have the right form.*) -Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \ -\ \\ parts (knows Spy evs); \ -\ B \\ bad; evs \\ otway |] \ -\ ==> \\X. Says B Server \ -\ {|NA, Agent A, Agent B, X, \ -\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ -\ \\ set evs"; -by (etac rev_mp 1); -by (parts_induct_tac 1); -by (ALLGOALS Blast_tac); -qed "Crypt_imp_OR2"; - - -(** The Nonce NB uniquely identifies B's message. **) - -Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \\ parts(knows Spy evs); \ -\ Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \\ parts(knows Spy evs); \ -\ evs \\ otway; B \\ bad |] \ -\ ==> NC = NA & C = A"; -by (etac rev_mp 1); -by (etac rev_mp 1); -by (parts_induct_tac 1); -(*Fake, OR2*) -by (REPEAT (Blast_tac 1)); -qed "unique_NB"; - -(*If the encrypted message appears, and B has used Nonce NB, - then it originated with the Server! Quite messy proof.*) -Goal "[| B \\ bad; evs \\ otway |] \ -\ ==> Crypt (shrK B) {|NB, Key K|} \\ parts (knows Spy evs) \ -\ --> (ALL X'. Says B Server \ -\ {|NA, Agent A, Agent B, X', \ -\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ -\ \\ set evs \ -\ --> Says Server B \ -\ {|NA, Crypt (shrK A) {|NA, Key K|}, \ -\ Crypt (shrK B) {|NB, Key K|}|} \ -\ \\ set evs)"; -by (asm_full_simp_tac (simpset() addsimps []) 1); -by (parts_induct_tac 1); -by (Blast_tac 1); -(*OR1: it cannot be a new Nonce, contradiction.*) -by (Blast_tac 1); -(*OR4*) -by (blast_tac (claset() addSDs [Crypt_imp_OR2]) 2); -(*OR3: needs AddSEs [MPair_parts] or it takes forever!*) -by (blast_tac (claset() addDs [unique_NB] - addEs [nonce_OR1_OR2_E]) 1); -qed_spec_mp "NB_Crypt_imp_Server_msg"; - - -(*Guarantee for B: if it gets a message with matching NB then the Server - has sent the correct message.*) -Goal "[| Says B Server {|NA, Agent A, Agent B, X', \ -\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ -\ \\ set evs; \ -\ Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \\ set evs; \ -\ B \\ bad; evs \\ otway |] \ -\ ==> Says Server B \ -\ {|NA, \ -\ Crypt (shrK A) {|NA, Key K|}, \ -\ Crypt (shrK B) {|NB, Key K|}|} \ -\ \\ set evs"; -by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1); -qed "B_trusts_OR3"; - - -(*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*) -Goal "[| Says B Server {|NA, Agent A, Agent B, X', \ -\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ -\ \\ set evs; \ -\ Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \\ set evs; \ -\ Notes Spy {|NA, NB, Key K|} \\ set evs; \ -\ A \\ bad; B \\ bad; evs \\ otway |] \ -\ ==> Key K \\ analz (knows Spy evs)"; -by (blast_tac (claset() addSDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1); -qed "B_gets_good_key"; - - -Goal "[| Says Server B \ -\ {|NA, Crypt (shrK A) {|NA, Key K|}, \ -\ Crypt (shrK B) {|NB, Key K|}|} \\ set evs; \ -\ B \\ bad; evs \\ otway |] \ -\ ==> \\X. Says B Server {|NA, Agent A, Agent B, X, \ -\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ -\ \\ set evs"; -by (etac rev_mp 1); -by (etac otway.induct 1); -by (ALLGOALS Asm_simp_tac); -by (blast_tac (claset() addSDs [Crypt_imp_OR2]) 3); -by (ALLGOALS Blast_tac); -qed "OR3_imp_OR2"; - - -(*After getting and checking OR4, agent A can trust that B has been active. - We could probably prove that X has the expected form, but that is not - strictly necessary for authentication.*) -Goal "[| Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} \\ set evs; \ -\ Says A B {|NA, Agent A, Agent B, \ -\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\ set evs; \ -\ A \\ bad; B \\ bad; evs \\ otway |] \ -\ ==> \\NB X. Says B Server {|NA, Agent A, Agent B, X, \ -\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}\ -\ \\ set evs"; -by (blast_tac (claset() delrules [Gets_imp_knows_Spy RS parts.Inj] - addSDs [A_trusts_OR4, OR3_imp_OR2]) 1); -qed "A_auths_B"; diff -r c8bbf4c4bc2d -r a6816d47f41d src/HOL/Auth/OtwayRees.thy --- a/src/HOL/Auth/OtwayRees.thy Wed Apr 11 11:53:54 2001 +0200 +++ b/src/HOL/Auth/OtwayRees.thy Thu Apr 12 12:45:05 2001 +0200 @@ -1,44 +1,49 @@ -(* +(* Title: HOL/Auth/OtwayRees + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge + Inductive relation "otway" for the Otway-Rees protocol extended by Gets primitive. Version that encrypts Nonce NB +From page 244 of + Burrows, Abadi and Needham. A Logic of Authentication. + Proc. Royal Soc. 426 (1989) *) -OtwayRees = Shared + +theory OtwayRees = Shared: -consts otway :: event list set +consts otway :: "event list set" inductive "otway" - intrs + intros (*Initial trace is empty*) - Nil "[] \\ otway" - - (** These rules allow agents to send messages to themselves **) + Nil: "[] \ otway" (*The spy MAY say anything he CAN say. We do not expect him to invent new nonces here, but he can also use NS1. Common to all similar protocols.*) - Fake "[| evsf \\ otway; X \\ synth (analz (knows Spy evsf)) |] - ==> Says Spy B X # evsf : otway" + Fake: "[| evsf \ otway; X \ synth (analz (knows Spy evsf)) |] + ==> Says Spy B X # evsf \ otway" (*A message that has been sent can be received by the intended recipient.*) - Reception "[| evsr \\ otway; Says A B X : set evsr |] - ==> Gets B X # evsr : otway" + Reception: "[| evsr \ otway; Says A B X \set evsr |] + ==> Gets B X # evsr \ otway" (*Alice initiates a protocol run*) - OR1 "[| evs1 \\ otway; Nonce NA \\ used evs1 |] - ==> Says A B {|Nonce NA, Agent A, Agent B, - Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} + OR1: "[| evs1 \ otway; Nonce NA \ used evs1 |] + ==> Says A B {|Nonce NA, Agent A, Agent B, + Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} # evs1 : otway" (*Bob's response to Alice's message. Note that NB is encrypted.*) - OR2 "[| evs2 \\ otway; Nonce NB \\ used evs2; + OR2: "[| evs2 \ otway; Nonce NB \ used evs2; Gets B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |] - ==> Says B Server - {|Nonce NA, Agent A, Agent B, X, + ==> Says B Server + {|Nonce NA, Agent A, Agent B, X, Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent B|}|} # evs2 : otway" @@ -46,23 +51,23 @@ (*The Server receives Bob's message and checks that the three NAs match. Then he sends a new session key to Bob with a packet for forwarding to Alice.*) - OR3 "[| evs3 \\ otway; Key KAB \\ used evs3; - Gets Server - {|Nonce NA, Agent A, Agent B, - Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, + OR3: "[| evs3 \ otway; Key KAB \ used evs3; + Gets Server + {|Nonce NA, Agent A, Agent B, + Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent B|}|} : set evs3 |] - ==> Says Server B - {|Nonce NA, + ==> Says Server B + {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key KAB|}, Crypt (shrK B) {|Nonce NB, Key KAB|}|} # evs3 : otway" (*Bob receives the Server's (?) message and compares the Nonces with those in the message he previously sent the Server. - Need B \\ Server because we allow messages to self.*) - OR4 "[| evs4 \\ otway; B \\ Server; - Says B Server {|Nonce NA, Agent A, Agent B, X', + Need B \ Server because we allow messages to self.*) + OR4: "[| evs4 \ otway; B \ Server; + Says B Server {|Nonce NA, Agent A, Agent B, X', Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent B|}|} : set evs4; @@ -72,9 +77,391 @@ (*This message models possible leaks of session keys. The nonces identify the protocol run.*) - Oops "[| evso \\ otway; + Oops: "[| evso \ otway; Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} : set evso |] ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway" + +declare Says_imp_knows_Spy [THEN analz.Inj, dest] +declare parts.Body [dest] +declare analz_into_parts [dest] +declare Fake_parts_insert_in_Un [dest] + + +(*A "possibility property": there are traces that reach the end*) +lemma "B \ Server + ==> \K. \evs \ otway. + Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} + \ set evs" +apply (intro exI bexI) +apply (rule_tac [2] otway.Nil + [THEN otway.OR1, THEN otway.Reception, + THEN otway.OR2, THEN otway.Reception, + THEN otway.OR3, THEN otway.Reception, THEN otway.OR4]) +apply possibility +done + +lemma Gets_imp_Says [dest!]: + "[| Gets B X \ set evs; evs \ otway |] ==> \A. Says A B X \ set evs" +apply (erule rev_mp) +apply (erule otway.induct) +apply auto +done + + +(**** Inductive proofs about otway ****) + +(** For reasoning about the encrypted portion of messages **) + +lemma OR2_analz_knows_Spy: + "[| Gets B {|N, Agent A, Agent B, X|} \ set evs; evs \ otway |] + ==> X \ analz (knows Spy evs)" +by blast + +lemma OR4_analz_knows_Spy: + "[| Gets B {|N, X, Crypt (shrK B) X'|} \ set evs; evs \ otway |] + ==> X \ analz (knows Spy evs)" +by blast + +(*These lemmas assist simplification by removing forwarded X-variables. + We can replace them by rewriting with parts_insert2 and proving using + dest: parts_cut, but the proofs become more difficult.*) +lemmas OR2_parts_knows_Spy = + OR2_analz_knows_Spy [THEN analz_into_parts, standard] + +(*There could be OR4_parts_knows_Spy and Oops_parts_knows_Spy, but for + some reason proofs work without them!*) + + +(** Theorems of the form X \ parts (knows Spy evs) imply that NOBODY + sends messages containing X! **) + +(*Spy never sees a good agent's shared key!*) +lemma Spy_see_shrK [simp]: + "evs \ otway ==> (Key (shrK A) \ parts (knows Spy evs)) = (A \ bad)" +apply (erule otway.induct, force, + drule_tac [4] OR2_parts_knows_Spy, simp_all) +apply blast+ +done + +lemma Spy_analz_shrK [simp]: + "evs \ otway ==> (Key (shrK A) \ analz (knows Spy evs)) = (A \ bad)" +by auto + +lemma Spy_see_shrK_D [dest!]: + "[|Key (shrK A) \ parts (knows Spy evs); evs \ otway|] ==> A \ bad" +by (blast dest: Spy_see_shrK) + + +(*** Proofs involving analz ***) + +(*Describes the form of K and NA when the Server sends this message. Also + for Oops case.*) +lemma Says_Server_message_form: + "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \ set evs; + evs \ otway |] + ==> K \ range shrK & (\i. NA = Nonce i) & (\j. NB = Nonce j)" +apply (erule rev_mp, erule otway.induct, simp_all) +apply blast +done + + +(**** + The following is to prove theorems of the form + + Key K \ analz (insert (Key KAB) (knows Spy evs)) ==> + Key K \ analz (knows Spy evs) + + A more general formula must be proved inductively. +****) + + +(** Session keys are not used to encrypt other session keys **) + +(*The equality makes the induction hypothesis easier to apply*) +lemma analz_image_freshK [rule_format]: + "evs \ otway ==> + \K KK. KK <= -(range shrK) --> + (Key K \ analz (Key`KK Un (knows Spy evs))) = + (K \ KK | Key K \ analz (knows Spy evs))" +apply (erule otway.induct, force) +apply (frule_tac [7] Says_Server_message_form) +apply (drule_tac [6] OR4_analz_knows_Spy) +apply (drule_tac [4] OR2_analz_knows_Spy) +apply analz_freshK +apply spy_analz +done + + +lemma analz_insert_freshK: + "[| evs \ otway; KAB \ range shrK |] ==> + Key K \ analz (insert (Key KAB) (knows Spy evs)) = + (K = KAB | Key K \ analz (knows Spy evs))" +by (simp only: analz_image_freshK analz_image_freshK_simps) + + +(*** The Key K uniquely identifies the Server's message. **) + +lemma unique_session_keys: + "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \ set evs; + Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \ set evs; + evs \ otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'" +apply (erule rev_mp) +apply (erule rev_mp) +apply (erule otway.induct, simp_all) +(*Remaining cases: OR3 and OR4*) +apply blast+ +done + + +(**** Authenticity properties relating to NA ****) + +(*Only OR1 can have caused such a part of a message to appear.*) +lemma Crypt_imp_OR1 [rule_format]: + "[| A \ bad; evs \ otway |] + ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \ parts (knows Spy evs) --> + Says A B {|NA, Agent A, Agent B, + Crypt (shrK A) {|NA, Agent A, Agent B|}|} + \ set evs" +apply (erule otway.induct, force, + drule_tac [4] OR2_parts_knows_Spy, simp_all) +apply blast+ +done + +lemma Crypt_imp_OR1_Gets: + "[| Gets B {|NA, Agent A, Agent B, + Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ set evs; + A \ bad; evs \ otway |] + ==> Says A B {|NA, Agent A, Agent B, + Crypt (shrK A) {|NA, Agent A, Agent B|}|} + \ set evs" +by (blast dest: Crypt_imp_OR1) + + +(** The Nonce NA uniquely identifies A's message. **) + +lemma unique_NA: + "[| Crypt (shrK A) {|NA, Agent A, Agent B|} \ parts (knows Spy evs); + Crypt (shrK A) {|NA, Agent A, Agent C|} \ parts (knows Spy evs); + evs \ otway; A \ bad |] + ==> B = C" +apply (erule rev_mp, erule rev_mp) +apply (erule otway.induct, force, + drule_tac [4] OR2_parts_knows_Spy, simp_all) +apply blast+ +done + + +(*It is impossible to re-use a nonce in both OR1 and OR2. This holds because + OR2 encrypts Nonce NB. It prevents the attack that can occur in the + over-simplified version of this protocol: see OtwayRees_Bad.*) +lemma no_nonce_OR1_OR2: + "[| Crypt (shrK A) {|NA, Agent A, Agent B|} \ parts (knows Spy evs); + A \ bad; evs \ otway |] + ==> Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \ parts (knows Spy evs)" +apply (erule rev_mp) +apply (erule otway.induct, force, + drule_tac [4] OR2_parts_knows_Spy, simp_all) +apply blast+ +done + +(*Crucial property: If the encrypted message appears, and A has used NA + to start a run, then it originated with the Server!*) +lemma NA_Crypt_imp_Server_msg [rule_format]: + "[| A \ bad; evs \ otway |] + ==> Says A B {|NA, Agent A, Agent B, + Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ set evs --> + Crypt (shrK A) {|NA, Key K|} \ parts (knows Spy evs) + --> (\NB. Says Server B + {|NA, + Crypt (shrK A) {|NA, Key K|}, + Crypt (shrK B) {|NB, Key K|}|} \ set evs)" +apply (erule otway.induct, force, + drule_tac [4] OR2_parts_knows_Spy, simp_all) +apply blast +(*OR1: it cannot be a new Nonce, contradiction.*) +apply blast +(*OR3*) +apply (blast dest!: no_nonce_OR1_OR2 intro: unique_NA) +(*OR4*) +apply (blast intro!: Crypt_imp_OR1) +done + + +(*Corollary: if A receives B's OR4 message and the nonce NA agrees + then the key really did come from the Server! CANNOT prove this of the + bad form of this protocol, even though we can prove + Spy_not_see_encrypted_key*) +lemma A_trusts_OR4: + "[| Says A B {|NA, Agent A, Agent B, + Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ set evs; + Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} \ set evs; + A \ bad; evs \ otway |] + ==> \NB. Says Server B + {|NA, + Crypt (shrK A) {|NA, Key K|}, + Crypt (shrK B) {|NB, Key K|}|} + \ set evs" +by (blast intro!: NA_Crypt_imp_Server_msg) + + +(** Crucial secrecy property: Spy does not see the keys sent in msg OR3 + Does not in itself guarantee security: an attack could violate + the premises, e.g. by having A=Spy **) + +lemma secrecy_lemma: + "[| A \ bad; B \ bad; evs \ otway |] + ==> Says Server B + {|NA, Crypt (shrK A) {|NA, Key K|}, + Crypt (shrK B) {|NB, Key K|}|} \ set evs --> + Notes Spy {|NA, NB, Key K|} \ set evs --> + Key K \ analz (knows Spy evs)" +apply (erule otway.induct, force) +apply (frule_tac [7] Says_Server_message_form) +apply (drule_tac [6] OR4_analz_knows_Spy) +apply (drule_tac [4] OR2_analz_knows_Spy) +apply (simp_all add: analz_insert_eq analz_insert_freshK pushes) +apply spy_analz (*Fake*) +(*OR3, OR4, Oops*) +apply (blast dest: unique_session_keys)+ +done + +lemma Spy_not_see_encrypted_key: + "[| Says Server B + {|NA, Crypt (shrK A) {|NA, Key K|}, + Crypt (shrK B) {|NB, Key K|}|} \ set evs; + Notes Spy {|NA, NB, Key K|} \ set evs; + A \ bad; B \ bad; evs \ otway |] + ==> Key K \ analz (knows Spy evs)" +by (blast dest: Says_Server_message_form secrecy_lemma) + + +(*A's guarantee. The Oops premise quantifies over NB because A cannot know + what it is.*) +lemma A_gets_good_key: + "[| Says A B {|NA, Agent A, Agent B, + Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ set evs; + Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} \ set evs; + \NB. Notes Spy {|NA, NB, Key K|} \ set evs; + A \ bad; B \ bad; evs \ otway |] + ==> Key K \ analz (knows Spy evs)" +by (blast dest!: A_trusts_OR4 Spy_not_see_encrypted_key) + + + +(**** Authenticity properties relating to NB ****) + +(*Only OR2 can have caused such a part of a message to appear. We do not + know anything about X: it does NOT have to have the right form.*) +lemma Crypt_imp_OR2: + "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \ parts (knows Spy evs); + B \ bad; evs \ otway |] + ==> \X. Says B Server + {|NA, Agent A, Agent B, X, + Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} + \ set evs" +apply (erule rev_mp) +apply (erule otway.induct, force, + drule_tac [4] OR2_parts_knows_Spy, simp_all) +apply blast+ +done + + +(** The Nonce NB uniquely identifies B's message. **) + +lemma unique_NB: + "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \ parts(knows Spy evs); + Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \ parts(knows Spy evs); + evs \ otway; B \ bad |] + ==> NC = NA & C = A" +apply (erule rev_mp, erule rev_mp) +apply (erule otway.induct, force, + drule_tac [4] OR2_parts_knows_Spy, simp_all) +(*Fake, OR2*) +apply blast+ +done + +(*If the encrypted message appears, and B has used Nonce NB, + then it originated with the Server! Quite messy proof.*) +lemma NB_Crypt_imp_Server_msg [rule_format]: + "[| B \ bad; evs \ otway |] + ==> Crypt (shrK B) {|NB, Key K|} \ parts (knows Spy evs) + --> (\X'. Says B Server + {|NA, Agent A, Agent B, X', + Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} + \ set evs + --> Says Server B + {|NA, Crypt (shrK A) {|NA, Key K|}, + Crypt (shrK B) {|NB, Key K|}|} + \ set evs)" +apply simp +apply (erule otway.induct, force, + drule_tac [4] OR2_parts_knows_Spy, simp_all) +apply blast +(*OR1: it cannot be a new Nonce, contradiction.*) +(*OR2*) +apply blast +(*OR3: needs elim: MPair_parts or it takes forever!*) +apply (blast dest: unique_NB dest!: no_nonce_OR1_OR2) +(*OR4*) +apply (blast dest!: Crypt_imp_OR2) +done + + +(*Guarantee for B: if it gets a message with matching NB then the Server + has sent the correct message.*) +lemma B_trusts_OR3: + "[| Says B Server {|NA, Agent A, Agent B, X', + Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} + \ set evs; + Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \ set evs; + B \ bad; evs \ otway |] + ==> Says Server B + {|NA, + Crypt (shrK A) {|NA, Key K|}, + Crypt (shrK B) {|NB, Key K|}|} + \ set evs" +by (blast intro!: NB_Crypt_imp_Server_msg) + + +(*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*) +lemma B_gets_good_key: + "[| Says B Server {|NA, Agent A, Agent B, X', + Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} + \ set evs; + Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \ set evs; + Notes Spy {|NA, NB, Key K|} \ set evs; + A \ bad; B \ bad; evs \ otway |] + ==> Key K \ analz (knows Spy evs)" +by (blast dest!: B_trusts_OR3 Spy_not_see_encrypted_key) + + +lemma OR3_imp_OR2: + "[| Says Server B + {|NA, Crypt (shrK A) {|NA, Key K|}, + Crypt (shrK B) {|NB, Key K|}|} \ set evs; + B \ bad; evs \ otway |] + ==> \X. Says B Server {|NA, Agent A, Agent B, X, + Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} + \ set evs" +apply (erule rev_mp) +apply (erule otway.induct, simp_all) +apply (blast dest!: Crypt_imp_OR2)+ +done + + +(*After getting and checking OR4, agent A can trust that B has been active. + We could probably prove that X has the expected form, but that is not + strictly necessary for authentication.*) +lemma A_auths_B: + "[| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} \ set evs; + Says A B {|NA, Agent A, Agent B, + Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ set evs; + A \ bad; B \ bad; evs \ otway |] + ==> \NB X. Says B Server {|NA, Agent A, Agent B, X, + Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} + \ set evs" +by (blast dest!: A_trusts_OR4 OR3_imp_OR2) + end diff -r c8bbf4c4bc2d -r a6816d47f41d src/HOL/Auth/OtwayRees_AN.ML --- a/src/HOL/Auth/OtwayRees_AN.ML Wed Apr 11 11:53:54 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,285 +0,0 @@ -(* Title: HOL/Auth/OtwayRees_AN - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1996 University of Cambridge - -Inductive relation "otway" for the Otway-Rees protocol. - -Abadi-Needham version: minimal encryption, explicit messages - -From page 11 of - Abadi and Needham. Prudent Engineering Practice for Cryptographic Protocols. - IEEE Trans. SE 22 (1), 1996 -*) - -AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body]; -AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; - - -(*A "possibility property": there are traces that reach the end*) -Goal "B \\ Server \ -\ ==> \\K. \\evs \\ otway. \ -\ Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \ -\ \\ set evs"; -by (REPEAT (resolve_tac [exI,bexI] 1)); -by (rtac (otway.Nil RS - otway.OR1 RS otway.Reception RS - otway.OR2 RS otway.Reception RS - otway.OR3 RS otway.Reception RS otway.OR4) 2); -by possibility_tac; -result(); - -Goal "[| Gets B X \\ set evs; evs \\ otway |] ==> \\A. Says A B X \\ set evs"; -by (etac rev_mp 1); -by (etac otway.induct 1); -by Auto_tac; -qed"Gets_imp_Says"; - -(*Must be proved separately for each protocol*) -Goal "[| Gets B X \\ set evs; evs \\ otway |] ==> X \\ knows Spy evs"; -by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1); -qed"Gets_imp_knows_Spy"; -AddDs [Gets_imp_knows_Spy RS parts.Inj]; - - -(**** Inductive proofs about otway ****) - -(** For reasoning about the encrypted portion of messages **) - -Goal "[| Gets B {|X, Crypt(shrK B) X'|} \\ set evs; evs \\ otway |] \ -\ ==> X \\ analz (knows Spy evs)"; -by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1); -qed "OR4_analz_knows_Spy"; - -Goal "Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \\ set evs \ -\ ==> K \\ parts (knows Spy evs)"; -by (Blast_tac 1); -qed "Oops_parts_knows_Spy"; - -bind_thm ("OR4_parts_knows_Spy", - OR4_analz_knows_Spy RS (impOfSubs analz_subset_parts)); - -(*For proving the easier theorems about X \\ parts (knows Spy evs).*) -fun parts_induct_tac i = - etac otway.induct i THEN - ftac Oops_parts_knows_Spy (i+7) THEN - ftac OR4_parts_knows_Spy (i+6) THEN - prove_simple_subgoals_tac i; - - -(** Theorems of the form X \\ parts (knows Spy evs) imply that NOBODY - sends messages containing X! **) - -(*Spy never sees a good agent's shared key!*) -Goal "evs \\ otway ==> (Key (shrK A) \\ parts (knows Spy evs)) = (A \\ bad)"; -by (parts_induct_tac 1); -by (ALLGOALS Blast_tac); -qed "Spy_see_shrK"; -Addsimps [Spy_see_shrK]; - -Goal "evs \\ otway ==> (Key (shrK A) \\ analz (knows Spy evs)) = (A \\ bad)"; -by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); -qed "Spy_analz_shrK"; -Addsimps [Spy_analz_shrK]; - -AddSDs [Spy_see_shrK RSN (2, rev_iffD1), - Spy_analz_shrK RSN (2, rev_iffD1)]; - - -(*** Proofs involving analz ***) - -(*Describes the form of K and NA when the Server sends this message.*) -Goal "[| Says Server B \ -\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ -\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ -\ \\ set evs; \ -\ evs \\ otway |] \ -\ ==> K \\ range shrK & (\\i. NA = Nonce i) & (\\j. NB = Nonce j)"; -by (etac rev_mp 1); -by (etac otway.induct 1); -by (ALLGOALS Asm_simp_tac); -by (Blast_tac 1); -qed "Says_Server_message_form"; - - -(*For proofs involving analz.*) -val analz_knows_Spy_tac = - dtac OR4_analz_knows_Spy 7 THEN assume_tac 7 THEN - ftac Says_Server_message_form 8 THEN assume_tac 8 THEN - REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 8); - - -(**** - The following is to prove theorems of the form - - Key K \\ analz (insert (Key KAB) (knows Spy evs)) ==> - Key K \\ analz (knows Spy evs) - - A more general formula must be proved inductively. -****) - - -(** Session keys are not used to encrypt other session keys **) - -(*The equality makes the induction hypothesis easier to apply*) -Goal "evs \\ otway ==> \ -\ ALL K KK. KK <= -(range shrK) --> \ -\ (Key K \\ analz (Key`KK Un (knows Spy evs))) = \ -\ (K \\ KK | Key K \\ analz (knows Spy evs))"; -by (etac otway.induct 1); -by analz_knows_Spy_tac; -by (REPEAT_FIRST (resolve_tac [allI, impI])); -by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); -by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); -(*Fake*) -by (spy_analz_tac 1); -qed_spec_mp "analz_image_freshK"; - - -Goal "[| evs \\ otway; KAB \\ range shrK |] ==> \ -\ Key K \\ analz (insert (Key KAB) (knows Spy evs)) = \ -\ (K = KAB | Key K \\ analz (knows Spy evs))"; -by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); -qed "analz_insert_freshK"; - - -(*** The Key K uniquely identifies the Server's message. **) - -Goal "[| Says Server B \ -\ {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, \ -\ Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} \ -\ \\ set evs; \ -\ Says Server B' \ -\ {|Crypt (shrK A') {|NA', Agent A', Agent B', K|}, \ -\ Crypt (shrK B') {|NB', Agent A', Agent B', K|}|} \ -\ \\ set evs; \ -\ evs \\ otway |] \ -\ ==> A=A' & B=B' & NA=NA' & NB=NB'"; -by (etac rev_mp 1); -by (etac rev_mp 1); -by (etac otway.induct 1); -by (ALLGOALS Asm_simp_tac); -(*Remaining cases: OR3 and OR4*) -by (REPEAT (Blast_tac 1)); -qed "unique_session_keys"; - - - -(**** Authenticity properties relating to NA ****) - -(*If the encrypted message appears then it originated with the Server!*) -Goal "[| A \\ bad; A \\ B; evs \\ otway |] \ -\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} \\ parts (knows Spy evs) \ -\ --> (\\NB. Says Server B \ -\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ -\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ -\ \\ set evs)"; -by (parts_induct_tac 1); -by (Blast_tac 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); -(*OR3*) -by (Blast_tac 1); -qed_spec_mp "NA_Crypt_imp_Server_msg"; - - -(*Corollary: if A receives B's OR4 message then it originated with the Server. - Freshness may be inferred from nonce NA.*) -Goal "[| Gets A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \ -\ \\ set evs; \ -\ A \\ bad; A \\ B; evs \\ otway |] \ -\ ==> \\NB. Says Server B \ -\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ -\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ -\ \\ set evs"; -by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1); -qed "A_trusts_OR4"; - - -(** Crucial secrecy property: Spy does not see the keys sent in msg OR3 - Does not in itself guarantee security: an attack could violate - the premises, e.g. by having A=Spy **) - -Goal "[| A \\ bad; B \\ bad; evs \\ otway |] \ -\ ==> Says Server B \ -\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ -\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ -\ \\ set evs --> \ -\ Notes Spy {|NA, NB, Key K|} \\ set evs --> \ -\ Key K \\ analz (knows Spy evs)"; -by (etac otway.induct 1); -by analz_knows_Spy_tac; -by (ALLGOALS - (asm_simp_tac (simpset() addcongs [conj_cong] - addsimps [analz_insert_eq, analz_insert_freshK] - @ pushes @ split_ifs))); -(*Oops*) -by (blast_tac (claset() addSDs [unique_session_keys]) 4); -(*OR4*) -by (Blast_tac 3); -(*OR3*) -by (Blast_tac 2); -(*Fake*) -by (spy_analz_tac 1); -val lemma = result() RS mp RS mp RSN(2,rev_notE); - -Goal "[| Says Server B \ -\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ -\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ -\ \\ set evs; \ -\ Notes Spy {|NA, NB, Key K|} \\ set evs; \ -\ A \\ bad; B \\ bad; evs \\ otway |] \ -\ ==> Key K \\ analz (knows Spy evs)"; -by (ftac Says_Server_message_form 1 THEN assume_tac 1); -by (blast_tac (claset() addSEs [lemma]) 1); -qed "Spy_not_see_encrypted_key"; - - -(*A's guarantee. The Oops premise quantifies over NB because A cannot know - what it is.*) -Goal "[| Gets A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \ -\ \\ set evs; \ -\ ALL NB. Notes Spy {|NA, NB, Key K|} \\ set evs; \ -\ A \\ bad; B \\ bad; A \\ B; evs \\ otway |] \ -\ ==> Key K \\ analz (knows Spy evs)"; -by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1); -qed "A_gets_good_key"; - - -(**** Authenticity properties relating to NB ****) - -(*If the encrypted message appears then it originated with the Server!*) -Goal "[| B \\ bad; A \\ B; evs \\ otway |] \ -\ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} \\ parts (knows Spy evs) \ -\ --> (\\NA. Says Server B \ -\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ -\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ -\ \\ set evs)"; -by (parts_induct_tac 1); -by (Blast_tac 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); -(*OR3*) -by (Blast_tac 1); -qed_spec_mp "NB_Crypt_imp_Server_msg"; - - -(*Guarantee for B: if it gets a well-formed certificate then the Server - has sent the correct message in round 3.*) -Goal "[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ -\ \\ set evs; \ -\ B \\ bad; A \\ B; evs \\ otway |] \ -\ ==> \\NA. Says Server B \ -\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ -\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ -\ \\ set evs"; -by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1); -qed "B_trusts_OR3"; - - -(*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*) -Goal "[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ -\ \\ set evs; \ -\ ALL NA. Notes Spy {|NA, NB, Key K|} \\ set evs; \ -\ A \\ bad; B \\ bad; A \\ B; evs \\ otway |] \ -\ ==> Key K \\ analz (knows Spy evs)"; -by (blast_tac (claset() addDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1); -qed "B_gets_good_key"; diff -r c8bbf4c4bc2d -r a6816d47f41d src/HOL/Auth/OtwayRees_AN.thy --- a/src/HOL/Auth/OtwayRees_AN.thy Wed Apr 11 11:53:54 2001 +0200 +++ b/src/HOL/Auth/OtwayRees_AN.thy Thu Apr 12 12:45:05 2001 +0200 @@ -5,7 +5,7 @@ Inductive relation "otway" for the Otway-Rees protocol. -Simplified version with minimal encryption but explicit messages +Abadi-Needham simplified version: minimal encryption, explicit messages Note that the formalization does not even assume that nonces are fresh. This is because the protocol does not rely on uniqueness of nonces for @@ -17,61 +17,298 @@ IEEE Trans. SE 22 (1), 1996 *) -OtwayRees_AN = Shared + +theory OtwayRees_AN = Shared: -consts otway :: event list set +consts otway :: "event list set" inductive "otway" - intrs + intros (*Initial trace is empty*) - Nil "[]: otway" + Nil: "[] \ otway" (*The spy MAY say anything he CAN say. We do not expect him to invent new nonces here, but he can also use NS1. Common to all similar protocols.*) - Fake "[| evs \\ otway; X \\ synth (analz (knows Spy evs)) |] - ==> Says Spy B X # evs \\ otway" + Fake: "[| evsf \ otway; X \ synth (analz (knows Spy evsf)) |] + ==> Says Spy B X # evsf \ otway" (*A message that has been sent can be received by the intended recipient.*) - Reception "[| evsr \\ otway; Says A B X \\set evsr |] - ==> Gets B X # evsr \\ otway" + Reception: "[| evsr \ otway; Says A B X \set evsr |] + ==> Gets B X # evsr \ otway" (*Alice initiates a protocol run*) - OR1 "[| evs1 \\ otway |] - ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs1 \\ otway" + OR1: "evs1 \ otway + ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs1 \ otway" (*Bob's response to Alice's message.*) - OR2 "[| evs2 \\ otway; - Gets B {|Agent A, Agent B, Nonce NA|} \\set evs2 |] + OR2: "[| evs2 \ otway; + Gets B {|Agent A, Agent B, Nonce NA|} \set evs2 |] ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} - # evs2 \\ otway" + # evs2 \ otway" (*The Server receives Bob's message. Then he sends a new session key to Bob with a packet for forwarding to Alice.*) - OR3 "[| evs3 \\ otway; Key KAB \\ used evs3; + OR3: "[| evs3 \ otway; Key KAB \ used evs3; Gets Server {|Agent A, Agent B, Nonce NA, Nonce NB|} - \\set evs3 |] - ==> Says Server B + \set evs3 |] + ==> Says Server B {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key KAB|}, Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key KAB|}|} - # evs3 \\ otway" + # evs3 \ otway" (*Bob receives the Server's (?) message and compares the Nonces with those in the message he previously sent the Server. - Need B \\ Server because we allow messages to self.*) - OR4 "[| evs4 \\ otway; B \\ Server; - Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} \\set evs4; + Need B \ Server because we allow messages to self.*) + OR4: "[| evs4 \ otway; B \ Server; + Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} \set evs4; Gets B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|} - \\set evs4 |] - ==> Says B A X # evs4 \\ otway" + \set evs4 |] + ==> Says B A X # evs4 \ otway" (*This message models possible leaks of session keys. The nonces identify the protocol run. B is not assumed to know shrK A.*) - Oops "[| evso \\ otway; - Says Server B - {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}, + Oops: "[| evso \ otway; + Says Server B + {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}, Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|} - \\set evso |] - ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \\ otway" + \set evso |] + ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \ otway" + + +declare Says_imp_knows_Spy [THEN analz.Inj, dest] +declare parts.Body [dest] +declare analz_into_parts [dest] +declare Fake_parts_insert_in_Un [dest] + + +(*A "possibility property": there are traces that reach the end*) +lemma "B \ Server + ==> \K. \evs \ otway. + Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) + \ set evs" +apply (intro exI bexI) +apply (rule_tac [2] otway.Nil + [THEN otway.OR1, THEN otway.Reception, + THEN otway.OR2, THEN otway.Reception, + THEN otway.OR3, THEN otway.Reception, THEN otway.OR4]) +apply possibility +done + +lemma Gets_imp_Says [dest!]: + "[| Gets B X \ set evs; evs \ otway |] ==> \A. Says A B X \ set evs" +by (erule rev_mp, erule otway.induct, auto) + + +(**** Inductive proofs about otway ****) + +(** For reasoning about the encrypted portion of messages **) + +lemma OR4_analz_knows_Spy: + "[| Gets B {|X, Crypt(shrK B) X'|} \ set evs; evs \ otway |] + ==> X \ analz (knows Spy evs)" +by blast + + +(** Theorems of the form X \ parts (knows Spy evs) imply that NOBODY + sends messages containing X! **) + +(*Spy never sees a good agent's shared key!*) +lemma Spy_see_shrK [simp]: + "evs \ otway ==> (Key (shrK A) \ parts (knows Spy evs)) = (A \ bad)" +apply (erule otway.induct, simp_all) +apply blast+ +done + +lemma Spy_analz_shrK [simp]: + "evs \ otway ==> (Key (shrK A) \ analz (knows Spy evs)) = (A \ bad)" +by auto + +lemma Spy_see_shrK_D [dest!]: + "[|Key (shrK A) \ parts (knows Spy evs); evs \ otway|] ==> A \ bad" +by (blast dest: Spy_see_shrK) + + +(*** Proofs involving analz ***) + +(*Describes the form of K and NA when the Server sends this message.*) +lemma Says_Server_message_form: + "[| Says Server B + {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, + Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} + \ set evs; + evs \ otway |] + ==> K \ range shrK & (\i. NA = Nonce i) & (\j. NB = Nonce j)" +apply (erule rev_mp) +apply (erule otway.induct) +apply simp_all +apply blast +done + + + +(**** + The following is to prove theorems of the form + + Key K \ analz (insert (Key KAB) (knows Spy evs)) ==> + Key K \ analz (knows Spy evs) + + A more general formula must be proved inductively. +****) + + +(** Session keys are not used to encrypt other session keys **) + +(*The equality makes the induction hypothesis easier to apply*) +lemma analz_image_freshK [rule_format]: + "evs \ otway ==> + \K KK. KK <= -(range shrK) --> + (Key K \ analz (Key`KK Un (knows Spy evs))) = + (K \ KK | Key K \ analz (knows Spy evs))" +apply (erule otway.induct, force) +apply (frule_tac [7] Says_Server_message_form) +apply (drule_tac [6] OR4_analz_knows_Spy) +apply analz_freshK +apply spy_analz +done + +lemma analz_insert_freshK: + "[| evs \ otway; KAB \ range shrK |] ==> + Key K \ analz (insert (Key KAB) (knows Spy evs)) = + (K = KAB | Key K \ analz (knows Spy evs))" +by (simp only: analz_image_freshK analz_image_freshK_simps) + + +(*** The Key K uniquely identifies the Server's message. **) + +lemma unique_session_keys: + "[| Says Server B + {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, + Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} + \ set evs; + Says Server B' + {|Crypt (shrK A') {|NA', Agent A', Agent B', K|}, + Crypt (shrK B') {|NB', Agent A', Agent B', K|}|} + \ set evs; + evs \ otway |] + ==> A=A' & B=B' & NA=NA' & NB=NB'" +apply (erule rev_mp, erule rev_mp, erule otway.induct) +apply simp_all +(*Remaining cases: OR3 and OR4*) +apply blast+ +done + + +(**** Authenticity properties relating to NA ****) + +(*If the encrypted message appears then it originated with the Server!*) +lemma NA_Crypt_imp_Server_msg [rule_format]: + "[| A \ bad; A \ B; evs \ otway |] + ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} \ parts (knows Spy evs) + --> (\NB. Says Server B + {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, + Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} + \ set evs)" +apply (erule otway.induct, force) +apply (simp_all add: ex_disj_distrib) +(*Fake, OR3*) +apply blast+; +done + + +(*Corollary: if A receives B's OR4 message then it originated with the Server. + Freshness may be inferred from nonce NA.*) +lemma A_trusts_OR4: + "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \ set evs; + A \ bad; A \ B; evs \ otway |] + ==> \NB. Says Server B + {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, + Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} + \ set evs" +by (blast intro!: NA_Crypt_imp_Server_msg) + + +(** Crucial secrecy property: Spy does not see the keys sent in msg OR3 + Does not in itself guarantee security: an attack could violate + the premises, e.g. by having A=Spy **) + +lemma secrecy_lemma: + "[| A \ bad; B \ bad; evs \ otway |] + ==> Says Server B + {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, + Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} + \ set evs --> + Notes Spy {|NA, NB, Key K|} \ set evs --> + Key K \ analz (knows Spy evs)" +apply (erule otway.induct, force) +apply (frule_tac [7] Says_Server_message_form) +apply (drule_tac [6] OR4_analz_knows_Spy) +apply (simp_all add: analz_insert_eq analz_insert_freshK pushes) +apply spy_analz (*Fake*) +(*OR3, OR4, Oops*) +apply (blast dest: unique_session_keys)+ +done + + +lemma Spy_not_see_encrypted_key: + "[| Says Server B + {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, + Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} + \ set evs; + Notes Spy {|NA, NB, Key K|} \ set evs; + A \ bad; B \ bad; evs \ otway |] + ==> Key K \ analz (knows Spy evs)" +by (blast dest: Says_Server_message_form secrecy_lemma) + + +(*A's guarantee. The Oops premise quantifies over NB because A cannot know + what it is.*) +lemma A_gets_good_key: + "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \ set evs; + \NB. Notes Spy {|NA, NB, Key K|} \ set evs; + A \ bad; B \ bad; A \ B; evs \ otway |] + ==> Key K \ analz (knows Spy evs)" +by (blast dest!: A_trusts_OR4 Spy_not_see_encrypted_key) + + + +(**** Authenticity properties relating to NB ****) + +(*If the encrypted message appears then it originated with the Server!*) + +lemma NB_Crypt_imp_Server_msg [rule_format]: + "[| B \ bad; A \ B; evs \ otway |] + ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} \ parts (knows Spy evs) + --> (\NA. Says Server B + {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, + Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} + \ set evs)" +apply (erule otway.induct, force, simp_all add: ex_disj_distrib) +(*Fake, OR3*) +apply blast+; +done + + + +(*Guarantee for B: if it gets a well-formed certificate then the Server + has sent the correct message in round 3.*) +lemma B_trusts_OR3: + "[| Says S B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} + \ set evs; + B \ bad; A \ B; evs \ otway |] + ==> \NA. Says Server B + {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, + Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} + \ set evs" +by (blast intro!: NB_Crypt_imp_Server_msg) + + +(*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*) +lemma B_gets_good_key: + "[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} + \ set evs; + \NA. Notes Spy {|NA, NB, Key K|} \ set evs; + A \ bad; B \ bad; A \ B; evs \ otway |] + ==> Key K \ analz (knows Spy evs)" +by (blast dest: B_trusts_OR3 Spy_not_see_encrypted_key) end diff -r c8bbf4c4bc2d -r a6816d47f41d src/HOL/Auth/OtwayRees_Bad.ML --- a/src/HOL/Auth/OtwayRees_Bad.ML Wed Apr 11 11:53:54 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,261 +0,0 @@ -(* Title: HOL/Auth/OtwayRees_Bad - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1996 University of Cambridge - -Inductive relation "otway" for the Otway-Rees protocol. - -The FAULTY version omitting encryption of Nonce NB, as suggested on page 247 of - Burrows, Abadi and Needham. A Logic of Authentication. - Proc. Royal Soc. 426 (1989) - -This file illustrates the consequences of such errors. We can still prove -impressive-looking properties such as Spy_not_see_encrypted_key, yet the -protocol is open to a middleperson attack. Attempting to prove some key lemmas -indicates the possibility of this attack. -*) - -AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body]; -AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; - -(*A "possibility property": there are traces that reach the end*) -Goal "B \\ Server \ -\ ==> \\K. \\NA. \\evs \\ otway. \ -\ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \ -\ \\ set evs"; -by (REPEAT (resolve_tac [exI,bexI] 1)); -by (rtac (otway.Nil RS - otway.OR1 RS otway.Reception RS - otway.OR2 RS otway.Reception RS - otway.OR3 RS otway.Reception RS otway.OR4) 2); -by possibility_tac; -result(); - -Goal "[| Gets B X \\ set evs; evs \\ otway |] ==> \\A. Says A B X \\ set evs"; -by (etac rev_mp 1); -by (etac otway.induct 1); -by Auto_tac; -qed"Gets_imp_Says"; - -(*Must be proved separately for each protocol*) -Goal "[| Gets B X \\ set evs; evs \\ otway |] ==> X \\ knows Spy evs"; -by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1); -qed"Gets_imp_knows_Spy"; -AddDs [Gets_imp_knows_Spy RS parts.Inj]; - - -(**** Inductive proofs about otway ****) - - -(** For reasoning about the encrypted portion of messages **) - -Goal "[| Gets B {|N, Agent A, Agent B, X|} \\ set evs; evs \\ otway |] \ -\ ==> X \\ analz (knows Spy evs)"; -by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1); -qed "OR2_analz_knows_Spy"; - -Goal "[| Gets B {|N, X, Crypt (shrK B) X'|} \\ set evs; evs \\ otway |] \ -\ ==> X \\ analz (knows Spy evs)"; -by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1); -qed "OR4_analz_knows_Spy"; - -Goal "Says Server B {|NA, X, Crypt K' {|NB,K|}|} \\ set evs \ -\ ==> K \\ parts (knows Spy evs)"; -by (Blast_tac 1); -qed "Oops_parts_knows_Spy"; - -bind_thm ("OR2_parts_knows_Spy", - OR2_analz_knows_Spy RS (impOfSubs analz_subset_parts)); -bind_thm ("OR4_parts_knows_Spy", - OR4_analz_knows_Spy RS (impOfSubs analz_subset_parts)); - -(*For proving the easier theorems about X \\ parts (knows Spy evs).*) -fun parts_induct_tac i = - etac otway.induct i THEN - ftac Oops_parts_knows_Spy (i+7) THEN - ftac OR4_parts_knows_Spy (i+6) THEN - ftac OR2_parts_knows_Spy (i+4) THEN - prove_simple_subgoals_tac i; - - -(** Theorems of the form X \\ parts (knows Spy evs) imply that NOBODY - sends messages containing X! **) - -(*Spy never sees a good agent's shared key!*) -Goal "evs \\ otway ==> (Key (shrK A) \\ parts (knows Spy evs)) = (A \\ bad)"; -by (parts_induct_tac 1); -by (ALLGOALS Blast_tac); -qed "Spy_see_shrK"; -Addsimps [Spy_see_shrK]; - -Goal "evs \\ otway ==> (Key (shrK A) \\ analz (knows Spy evs)) = (A \\ bad)"; -by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); -qed "Spy_analz_shrK"; -Addsimps [Spy_analz_shrK]; - -AddSDs [Spy_see_shrK RSN (2, rev_iffD1), - Spy_analz_shrK RSN (2, rev_iffD1)]; - - -(*** Proofs involving analz ***) - -(*Describes the form of K and NA when the Server sends this message. Also - for Oops case.*) -Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \\ set evs; \ -\ evs \\ otway |] \ -\ ==> K \\ range shrK & (\\i. NA = Nonce i) & (\\j. NB = Nonce j)"; -by (etac rev_mp 1); -by (etac otway.induct 1); -by (ALLGOALS Simp_tac); -by (ALLGOALS Blast_tac); -qed "Says_Server_message_form"; - - -(*For proofs involving analz.*) -val analz_knows_Spy_tac = - dtac OR2_analz_knows_Spy 5 THEN assume_tac 5 THEN - dtac OR4_analz_knows_Spy 7 THEN assume_tac 7 THEN - ftac Says_Server_message_form 8 THEN assume_tac 8 THEN - REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 8); - - -(**** - The following is to prove theorems of the form - - Key K \\ analz (insert (Key KAB) (knows Spy evs)) ==> - Key K \\ analz (knows Spy evs) - - A more general formula must be proved inductively. -****) - - -(** Session keys are not used to encrypt other session keys **) - -(*The equality makes the induction hypothesis easier to apply*) -Goal "evs \\ otway ==> \ -\ \\K KK. KK <= - (range shrK) --> \ -\ (Key K \\ analz (Key`KK Un (knows Spy evs))) = \ -\ (K \\ KK | Key K \\ analz (knows Spy evs))"; -by (etac otway.induct 1); -by analz_knows_Spy_tac; -by (REPEAT_FIRST (resolve_tac [allI, impI])); -by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); -by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); -(*Fake*) -by (spy_analz_tac 1); -qed_spec_mp "analz_image_freshK"; - - -Goal "[| evs \\ otway; KAB \\ range shrK |] ==> \ -\ Key K \\ analz (insert (Key KAB) (knows Spy evs)) = \ -\ (K = KAB | Key K \\ analz (knows Spy evs))"; -by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); -qed "analz_insert_freshK"; - - -(*** The Key K uniquely identifies the Server's message. **) - -Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \\ set evs; \ -\ Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \\ set evs; \ -\ evs \\ otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'"; -by (etac rev_mp 1); -by (etac rev_mp 1); -by (etac otway.induct 1); -by (ALLGOALS Asm_simp_tac); -(*Remaining cases: OR3 and OR4*) -by (REPEAT (Blast_tac 1)); -qed "unique_session_keys"; - - -(** Crucial secrecy property: Spy does not see the keys sent in msg OR3 - Does not in itself guarantee security: an attack could violate - the premises, e.g. by having A=Spy **) - -Goal "[| A \\ bad; B \\ bad; evs \\ otway |] \ -\ ==> Says Server B \ -\ {|NA, Crypt (shrK A) {|NA, Key K|}, \ -\ Crypt (shrK B) {|NB, Key K|}|} \\ set evs --> \ -\ Notes Spy {|NA, NB, Key K|} \\ set evs --> \ -\ Key K \\ analz (knows Spy evs)"; -by (etac otway.induct 1); -by analz_knows_Spy_tac; -by (ALLGOALS - (asm_simp_tac (simpset() addcongs [conj_cong] - addsimps [analz_insert_eq, analz_insert_freshK] - @ pushes @ split_ifs))); -(*Oops*) -by (blast_tac (claset() addSDs [unique_session_keys]) 4); -(*OR4*) -by (Blast_tac 3); -(*OR3*) -by (Blast_tac 2); -(*Fake*) -by (spy_analz_tac 1); -val lemma = result() RS mp RS mp RSN(2,rev_notE); - -Goal "[| Says Server B \ -\ {|NA, Crypt (shrK A) {|NA, Key K|}, \ -\ Crypt (shrK B) {|NB, Key K|}|} \\ set evs; \ -\ Notes Spy {|NA, NB, Key K|} \\ set evs; \ -\ A \\ bad; B \\ bad; evs \\ otway |] \ -\ ==> Key K \\ analz (knows Spy evs)"; -by (ftac Says_Server_message_form 1 THEN assume_tac 1); -by (blast_tac (claset() addSEs [lemma]) 1); -qed "Spy_not_see_encrypted_key"; - - -(*** Attempting to prove stronger properties ***) - -(*Only OR1 can have caused such a part of a message to appear. - The premise A \\ B prevents OR2's similar-looking cryptogram from being - picked up. Original Otway-Rees doesn't need it.*) -Goal "[| A \\ bad; A \\ B; evs \\ otway |] \ -\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \\ parts (knows Spy evs) --> \ -\ Says A B {|NA, Agent A, Agent B, \ -\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\ set evs"; -by (parts_induct_tac 1); -by (ALLGOALS Blast_tac); -qed_spec_mp "Crypt_imp_OR1"; - - -(*Crucial property: If the encrypted message appears, and A has used NA - to start a run, then it originated with the Server! - The premise A \\ B allows use of Crypt_imp_OR1*) -(*Only it is FALSE. Somebody could make a fake message to Server - substituting some other nonce NA' for NB.*) -Goal "[| A \\ bad; A \\ B; evs \\ otway |] \ -\ ==> Crypt (shrK A) {|NA, Key K|} \\ parts (knows Spy evs) --> \ -\ Says A B {|NA, Agent A, Agent B, \ -\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ -\ \\ set evs --> \ -\ (\\B NB. Says Server B \ -\ {|NA, \ -\ Crypt (shrK A) {|NA, Key K|}, \ -\ Crypt (shrK B) {|NB, Key K|}|} \\ set evs)"; -by (parts_induct_tac 1); -(*Fake*) -by (Blast_tac 1); -(*OR1: it cannot be a new Nonce, contradiction.*) -by (Blast_tac 1); -(*OR3 and OR4*) -by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); -by (ALLGOALS Clarify_tac); -(*OR4*) -by (blast_tac (claset() addSIs [Crypt_imp_OR1]) 2); -(*OR3*) (** LEVEL 5 **) -(*The hypotheses at this point suggest an attack in which nonce NB is used - in two different roles: - Gets Server - {|Nonce NA, Agent Aa, Agent A, - Crypt (shrK Aa) {|Nonce NA, Agent Aa, Agent A|}, Nonce NB, - Crypt (shrK A) {|Nonce NA, Agent Aa, Agent A|}|} - \\ set evs3; - Says A B - {|Nonce NB, Agent A, Agent B, - Crypt (shrK A) {|Nonce NB, Agent A, Agent B|}|} - \\ set evs3; -*) -writeln "GIVE UP! on NA_Crypt_imp_Server_msg"; - - -(*Thus the key property A_can_trust probably fails too.*) diff -r c8bbf4c4bc2d -r a6816d47f41d src/HOL/Auth/OtwayRees_Bad.thy --- a/src/HOL/Auth/OtwayRees_Bad.thy Wed Apr 11 11:53:54 2001 +0200 +++ b/src/HOL/Auth/OtwayRees_Bad.thy Thu Apr 12 12:45:05 2001 +0200 @@ -8,75 +8,304 @@ The FAULTY version omitting encryption of Nonce NB, as suggested on page 247 of Burrows, Abadi and Needham. A Logic of Authentication. Proc. Royal Soc. 426 (1989) + +This file illustrates the consequences of such errors. We can still prove +impressive-looking properties such as Spy_not_see_encrypted_key, yet the +protocol is open to a middleperson attack. Attempting to prove some key lemmas +indicates the possibility of this attack. *) -OtwayRees_Bad = Shared + - -consts otway :: event list set +theory OtwayRees_Bad = Shared: -inductive otway - intrs +consts otway :: "event list set" +inductive "otway" + intros (*Initial trace is empty*) - Nil "[] \\ otway" + Nil: "[] \ otway" (*The spy MAY say anything he CAN say. We do not expect him to invent new nonces here, but he can also use NS1. Common to all similar protocols.*) - Fake "[| evsf \\ otway; X \\ synth (analz (knows Spy evsf)) |] - ==> Says Spy B X # evsf \\ otway" + Fake: "[| evsf \ otway; X \ synth (analz (knows Spy evsf)) |] + ==> Says Spy B X # evsf \ otway" (*A message that has been sent can be received by the intended recipient.*) - Reception "[| evsr \\ otway; Says A B X \\ set evsr |] - ==> Gets B X # evsr \\ otway" + Reception: "[| evsr \ otway; Says A B X \set evsr |] + ==> Gets B X # evsr \ otway" (*Alice initiates a protocol run*) - OR1 "[| evs1 \\ otway; Nonce NA \\ used evs1 |] - ==> Says A B {|Nonce NA, Agent A, Agent B, - Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} - # evs1 \\ otway" + OR1: "[| evs1 \ otway; Nonce NA \ used evs1 |] + ==> Says A B {|Nonce NA, Agent A, Agent B, + Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} + # evs1 \ otway" - (*Bob's response to Alice's message. + (*Bob's response to Alice's message. This variant of the protocol does NOT encrypt NB.*) - OR2 "[| evs2 \\ otway; Nonce NB \\ used evs2; - Gets B {|Nonce NA, Agent A, Agent B, X|} \\ set evs2 |] - ==> Says B Server + OR2: "[| evs2 \ otway; Nonce NB \ used evs2; + Gets B {|Nonce NA, Agent A, Agent B, X|} \ set evs2 |] + ==> Says B Server {|Nonce NA, Agent A, Agent B, X, Nonce NB, Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} - # evs2 \\ otway" + # evs2 \ otway" (*The Server receives Bob's message and checks that the three NAs match. Then he sends a new session key to Bob with a packet for forwarding to Alice.*) - OR3 "[| evs3 \\ otway; Key KAB \\ used evs3; - Gets Server - {|Nonce NA, Agent A, Agent B, - Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, - Nonce NB, + OR3: "[| evs3 \ otway; Key KAB \ used evs3; + Gets Server + {|Nonce NA, Agent A, Agent B, + Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, + Nonce NB, Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} - \\ set evs3 |] - ==> Says Server B - {|Nonce NA, + \ set evs3 |] + ==> Says Server B + {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key KAB|}, Crypt (shrK B) {|Nonce NB, Key KAB|}|} - # evs3 \\ otway" + # evs3 \ otway" (*Bob receives the Server's (?) message and compares the Nonces with those in the message he previously sent the Server. Need B ~= Server because we allow messages to self.*) - OR4 "[| evs4 \\ otway; B ~= Server; + OR4: "[| evs4 \ otway; B ~= Server; Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} - \\ set evs4; + \ set evs4; Gets B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} - \\ set evs4 |] - ==> Says B A {|Nonce NA, X|} # evs4 \\ otway" + \ set evs4 |] + ==> Says B A {|Nonce NA, X|} # evs4 \ otway" (*This message models possible leaks of session keys. The nonces identify the protocol run.*) - Oops "[| evso \\ otway; + Oops: "[| evso \ otway; Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} - \\ set evso |] - ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \\ otway" + \ set evso |] + ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \ otway" + + +declare Says_imp_knows_Spy [THEN analz.Inj, dest] +declare parts.Body [dest] +declare analz_into_parts [dest] +declare Fake_parts_insert_in_Un [dest] + +(*A "possibility property": there are traces that reach the end*) +lemma "B \ Server + ==> \K. \NA. \evs \ otway. + Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} + \ set evs" +apply (intro exI bexI) +apply (rule_tac [2] otway.Nil + [THEN otway.OR1, THEN otway.Reception, + THEN otway.OR2, THEN otway.Reception, + THEN otway.OR3, THEN otway.Reception, THEN otway.OR4]) +apply possibility +done + +lemma Gets_imp_Says [dest!]: + "[| Gets B X \ set evs; evs \ otway |] ==> \A. Says A B X \ set evs" +apply (erule rev_mp) +apply (erule otway.induct) +apply auto +done + + +(**** Inductive proofs about otway ****) + + +(** For reasoning about the encrypted portion of messages **) + +lemma OR2_analz_knows_Spy: + "[| Gets B {|N, Agent A, Agent B, X|} \ set evs; evs \ otway |] + ==> X \ analz (knows Spy evs)" +by blast + +lemma OR4_analz_knows_Spy: + "[| Gets B {|N, X, Crypt (shrK B) X'|} \ set evs; evs \ otway |] + ==> X \ analz (knows Spy evs)" +by blast + +lemma Oops_parts_knows_Spy: + "Says Server B {|NA, X, Crypt K' {|NB,K|}|} \ set evs + ==> K \ parts (knows Spy evs)" +by blast + +(*Forwarding lemma: see comments in OtwayRees.thy*) +lemmas OR2_parts_knows_Spy = + OR2_analz_knows_Spy [THEN analz_into_parts, standard] + + +(** Theorems of the form X \ parts (knows Spy evs) imply that NOBODY + sends messages containing X! **) + +(*Spy never sees a good agent's shared key!*) +lemma Spy_see_shrK [simp]: + "evs \ otway ==> (Key (shrK A) \ parts (knows Spy evs)) = (A \ bad)" +apply (erule otway.induct, force, + drule_tac [4] OR2_parts_knows_Spy, simp_all) +apply blast+ +done + +lemma Spy_analz_shrK [simp]: + "evs \ otway ==> (Key (shrK A) \ analz (knows Spy evs)) = (A \ bad)" +by auto + +lemma Spy_see_shrK_D [dest!]: + "[|Key (shrK A) \ parts (knows Spy evs); evs \ otway|] ==> A \ bad" +by (blast dest: Spy_see_shrK) + + +(*** Proofs involving analz ***) + +(*Describes the form of K and NA when the Server sends this message. Also + for Oops case.*) +lemma Says_Server_message_form: + "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \ set evs; + evs \ otway |] + ==> K \ range shrK & (\i. NA = Nonce i) & (\j. NB = Nonce j)" +apply (erule rev_mp) +apply (erule otway.induct, simp_all) +apply blast +done + + +(**** + The following is to prove theorems of the form + + Key K \ analz (insert (Key KAB) (knows Spy evs)) ==> + Key K \ analz (knows Spy evs) + + A more general formula must be proved inductively. +****) + + +(** Session keys are not used to encrypt other session keys **) + +(*The equality makes the induction hypothesis easier to apply*) +lemma analz_image_freshK [rule_format]: + "evs \ otway ==> + \K KK. KK <= -(range shrK) --> + (Key K \ analz (Key`KK Un (knows Spy evs))) = + (K \ KK | Key K \ analz (knows Spy evs))" +apply (erule otway.induct, force) +apply (frule_tac [7] Says_Server_message_form) +apply (drule_tac [6] OR4_analz_knows_Spy) +apply (drule_tac [4] OR2_analz_knows_Spy) +apply analz_freshK +apply spy_analz +done + +lemma analz_insert_freshK: + "[| evs \ otway; KAB \ range shrK |] ==> + Key K \ analz (insert (Key KAB) (knows Spy evs)) = + (K = KAB | Key K \ analz (knows Spy evs))" +by (simp only: analz_image_freshK analz_image_freshK_simps) + + +(*** The Key K uniquely identifies the Server's message. **) + +lemma unique_session_keys: + "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \ set evs; + Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \ set evs; + evs \ otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'" +apply (erule rev_mp) +apply (erule rev_mp) +apply (erule otway.induct, simp_all) +(*Remaining cases: OR3 and OR4*) +apply blast+ +done + + +(** Crucial secrecy property: Spy does not see the keys sent in msg OR3 + Does not in itself guarantee security: an attack could violate + the premises, e.g. by having A=Spy **) + +lemma secrecy_lemma: + "[| A \ bad; B \ bad; evs \ otway |] + ==> Says Server B + {|NA, Crypt (shrK A) {|NA, Key K|}, + Crypt (shrK B) {|NB, Key K|}|} \ set evs --> + Notes Spy {|NA, NB, Key K|} \ set evs --> + Key K \ analz (knows Spy evs)" +apply (erule otway.induct, force) +apply (frule_tac [7] Says_Server_message_form) +apply (drule_tac [6] OR4_analz_knows_Spy) +apply (drule_tac [4] OR2_analz_knows_Spy) +apply (simp_all add: analz_insert_eq analz_insert_freshK pushes) +apply spy_analz (*Fake*) +(*OR3, OR4, Oops*) +apply (blast dest: unique_session_keys)+ +done + + +lemma Spy_not_see_encrypted_key: + "[| Says Server B + {|NA, Crypt (shrK A) {|NA, Key K|}, + Crypt (shrK B) {|NB, Key K|}|} \ set evs; + Notes Spy {|NA, NB, Key K|} \ set evs; + A \ bad; B \ bad; evs \ otway |] + ==> Key K \ analz (knows Spy evs)" +by (blast dest: Says_Server_message_form secrecy_lemma) + + +(*** Attempting to prove stronger properties ***) + +(*Only OR1 can have caused such a part of a message to appear. + The premise A \ B prevents OR2's similar-looking cryptogram from being + picked up. Original Otway-Rees doesn't need it.*) +lemma Crypt_imp_OR1 [rule_format]: + "[| A \ bad; A \ B; evs \ otway |] + ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \ parts (knows Spy evs) --> + Says A B {|NA, Agent A, Agent B, + Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ set evs" +apply (erule otway.induct, force, + drule_tac [4] OR2_parts_knows_Spy, simp_all) +apply blast+ +done + + +(*Crucial property: If the encrypted message appears, and A has used NA + to start a run, then it originated with the Server! + The premise A \ B allows use of Crypt_imp_OR1*) +(*Only it is FALSE. Somebody could make a fake message to Server + substituting some other nonce NA' for NB.*) +lemma "[| A \ bad; A \ B; evs \ otway |] + ==> Crypt (shrK A) {|NA, Key K|} \ parts (knows Spy evs) --> + Says A B {|NA, Agent A, Agent B, + Crypt (shrK A) {|NA, Agent A, Agent B|}|} + \ set evs --> + (\B NB. Says Server B + {|NA, + Crypt (shrK A) {|NA, Key K|}, + Crypt (shrK B) {|NB, Key K|}|} \ set evs)" +apply (erule otway.induct, force, + drule_tac [4] OR2_parts_knows_Spy) +apply simp_all +(*Fake*) +apply blast +(*OR1: it cannot be a new Nonce, contradiction.*) +apply blast +(*OR3 and OR4*) +apply (simp_all add: ex_disj_distrib) +(*OR4*) +prefer 2 apply (blast intro!: Crypt_imp_OR1) +(*OR3*) +apply clarify +(*The hypotheses at this point suggest an attack in which nonce NB is used + in two different roles: + Gets Server + {|Nonce NA, Agent Aa, Agent A, + Crypt (shrK Aa) {|Nonce NA, Agent Aa, Agent A|}, Nonce NB, + Crypt (shrK A) {|Nonce NA, Agent Aa, Agent A|}|} + \ set evs3 + Says A B + {|Nonce NB, Agent A, Agent B, + Crypt (shrK A) {|Nonce NB, Agent A, Agent B|}|} + \ set evs3; +*) + + +(*Thus the key property A_can_trust probably fails too.*) +oops end diff -r c8bbf4c4bc2d -r a6816d47f41d src/HOL/Auth/WooLam.ML --- a/src/HOL/Auth/WooLam.ML Wed Apr 11 11:53:54 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,142 +0,0 @@ -(* Title: HOL/Auth/WooLam - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1996 University of Cambridge - -Inductive relation "woolam" for the Woo-Lam protocol. - -Simplified version from page 11 of - Abadi and Needham. Prudent Engineering Practice for Cryptographic Protocols. - IEEE Trans. S.E. 22(1), 1996, pages 6-15. -*) - -AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body]; -AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; - - -(*A "possibility property": there are traces that reach the end*) -Goal "\\NB. \\evs \\ woolam. \ -\ Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) \\ set evs"; -by (REPEAT (resolve_tac [exI,bexI] 1)); -by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS - woolam.WL4 RS woolam.WL5) 2); -by possibility_tac; -result(); - - -(**** Inductive proofs about woolam ****) - -(** For reasoning about the encrypted portion of messages **) - -Goal "Says A' B X \\ set evs ==> X \\ analz (spies evs)"; -by (etac (Says_imp_spies RS analz.Inj) 1); -qed "WL4_analz_spies"; - -bind_thm ("WL4_parts_spies", - WL4_analz_spies RS (impOfSubs analz_subset_parts)); - -(*For proving the easier theorems about X \\ parts (spies evs) *) -fun parts_induct_tac i = - etac woolam.induct i THEN - ftac WL4_parts_spies (i+5) THEN - prove_simple_subgoals_tac 1; - - -(** Theorems of the form X \\ parts (spies evs) imply that NOBODY - sends messages containing X! **) - -(*Spy never sees another agent's shared key! (unless it's bad at start)*) -Goal "evs \\ woolam ==> (Key (shrK A) \\ parts (spies evs)) = (A \\ bad)"; -by (parts_induct_tac 1); -by (Blast_tac 1); -qed "Spy_see_shrK"; -Addsimps [Spy_see_shrK]; - -Goal "evs \\ woolam ==> (Key (shrK A) \\ analz (spies evs)) = (A \\ bad)"; -by Auto_tac; -qed "Spy_analz_shrK"; -Addsimps [Spy_analz_shrK]; - -AddSDs [Spy_see_shrK RSN (2, rev_iffD1), - Spy_analz_shrK RSN (2, rev_iffD1)]; - - -(**** Autheticity properties for Woo-Lam ****) - - -(*** WL4 ***) - -(*If the encrypted message appears then it originated with Alice*) -Goal "[| Crypt (shrK A) (Nonce NB) \\ parts (spies evs); \ -\ A \\ bad; evs \\ woolam |] \ -\ ==> \\B. Says A B (Crypt (shrK A) (Nonce NB)) \\ set evs"; -by (etac rev_mp 1); -by (parts_induct_tac 1); -by (ALLGOALS Blast_tac); -qed "NB_Crypt_imp_Alice_msg"; - -(*Guarantee for Server: if it gets a message containing a certificate from - Alice, then she originated that certificate. But we DO NOT know that B - ever saw it: the Spy may have rerouted the message to the Server.*) -Goal "[| Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \ -\ \\ set evs; \ -\ A \\ bad; evs \\ woolam |] \ -\ ==> \\B. Says A B (Crypt (shrK A) (Nonce NB)) \\ set evs"; -by (blast_tac (claset() addSIs [NB_Crypt_imp_Alice_msg]) 1); -qed "Server_trusts_WL4"; - -AddDs [Server_trusts_WL4]; - - -(*** WL5 ***) - -(*Server sent WL5 only if it received the right sort of message*) -Goal "[| Says Server B (Crypt (shrK B) {|Agent A, NB|}) \\ set evs; \ -\ evs \\ woolam |] \ -\ ==> \\B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \ -\ \\ set evs"; -by (etac rev_mp 1); -by (parts_induct_tac 1); -by (ALLGOALS Blast_tac); -qed "Server_sent_WL5"; - -AddDs [Server_sent_WL5]; - -(*If the encrypted message appears then it originated with the Server!*) -Goal "[| Crypt (shrK B) {|Agent A, NB|} \\ parts (spies evs); \ -\ B \\ bad; evs \\ woolam |] \ -\ ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) \\ set evs"; -by (etac rev_mp 1); -by (parts_induct_tac 1); -by (Blast_tac 1); -qed_spec_mp "NB_Crypt_imp_Server_msg"; - -(*Guarantee for B. If B gets the Server's certificate then A has encrypted - the nonce using her key. This event can be no older than the nonce itself. - But A may have sent the nonce to some other agent and it could have reached - the Server via the Spy.*) -Goal "[| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs; \ -\ A \\ bad; B \\ bad; evs \\ woolam |] \ -\ ==> \\B. Says A B (Crypt (shrK A) (Nonce NB)) \\ set evs"; -by (blast_tac (claset() addSDs [NB_Crypt_imp_Server_msg]) 1); -qed "B_trusts_WL5"; - - -(*B only issues challenges in response to WL1. Not used.*) -Goal "[| Says B A (Nonce NB) \\ set evs; B \\ Spy; evs \\ woolam |] \ -\ ==> \\A'. Says A' B (Agent A) \\ set evs"; -by (etac rev_mp 1); -by (parts_induct_tac 1); -by (ALLGOALS Blast_tac); -qed "B_said_WL2"; - - -(**CANNOT be proved because A doesn't know where challenges come from... -Goal "[| A \\ bad; B \\ Spy; evs \\ woolam |] \ -\ ==> Crypt (shrK A) (Nonce NB) \\ parts (spies evs) & \ -\ Says B A (Nonce NB) \\ set evs \ -\ --> Says A B (Crypt (shrK A) (Nonce NB)) \\ set evs"; -by (parts_induct_tac 1); -by (Blast_tac 1); -by Safe_tac; -**) diff -r c8bbf4c4bc2d -r a6816d47f41d src/HOL/Auth/WooLam.thy --- a/src/HOL/Auth/WooLam.thy Wed Apr 11 11:53:54 2001 +0200 +++ b/src/HOL/Auth/WooLam.thy Thu Apr 12 12:45:05 2001 +0200 @@ -14,52 +14,166 @@ Computer Security Foundations Workshop, 1996. *) -WooLam = Shared + +theory WooLam = Shared: -consts woolam :: event list set +consts woolam :: "event list set" inductive woolam - intrs + intros (*Initial trace is empty*) - Nil "[] \\ woolam" + Nil: "[] \ woolam" (** These rules allow agents to send messages to themselves **) (*The spy MAY say anything he CAN say. We do not expect him to invent new nonces here, but he can also use NS1. Common to all similar protocols.*) - Fake "[| evsf \\ woolam; X \\ synth (analz (spies evsf)) |] - ==> Says Spy B X # evsf \\ woolam" + Fake: "[| evsf \ woolam; X \ synth (analz (spies evsf)) |] + ==> Says Spy B X # evsf \ woolam" (*Alice initiates a protocol run*) - WL1 "[| evs1 \\ woolam |] - ==> Says A B (Agent A) # evs1 \\ woolam" + WL1: "evs1 \ woolam ==> Says A B (Agent A) # evs1 \ woolam" (*Bob responds to Alice's message with a challenge.*) - WL2 "[| evs2 \\ woolam; Says A' B (Agent A) \\ set evs2 |] - ==> Says B A (Nonce NB) # evs2 \\ woolam" + WL2: "[| evs2 \ woolam; Says A' B (Agent A) \ set evs2 |] + ==> Says B A (Nonce NB) # evs2 \ woolam" (*Alice responds to Bob's challenge by encrypting NB with her key. B is *not* properly determined -- Alice essentially broadcasts her reply.*) - WL3 "[| evs3 \\ woolam; - Says A B (Agent A) \\ set evs3; - Says B' A (Nonce NB) \\ set evs3 |] - ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 \\ woolam" + WL3: "[| evs3 \ woolam; + Says A B (Agent A) \ set evs3; + Says B' A (Nonce NB) \ set evs3 |] + ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 \ woolam" (*Bob forwards Alice's response to the Server. NOTE: usually the messages are shown in chronological order, for clarity. But here, exchanging the two events would cause the lemma WL4_analz_spies to pick up the wrong assumption!*) - WL4 "[| evs4 \\ woolam; - Says A' B X \\ set evs4; - Says A'' B (Agent A) \\ set evs4 |] - ==> Says B Server {|Agent A, Agent B, X|} # evs4 \\ woolam" + WL4: "[| evs4 \ woolam; + Says A' B X \ set evs4; + Says A'' B (Agent A) \ set evs4 |] + ==> Says B Server {|Agent A, Agent B, X|} # evs4 \ woolam" (*Server decrypts Alice's response for Bob.*) - WL5 "[| evs5 \\ woolam; + WL5: "[| evs5 \ woolam; Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} - \\ set evs5 |] + \ set evs5 |] ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) - # evs5 \\ woolam" + # evs5 \ woolam" + + +declare Says_imp_knows_Spy [THEN analz.Inj, dest] +declare parts.Body [dest] +declare analz_into_parts [dest] +declare Fake_parts_insert_in_Un [dest] + + +(*A "possibility property": there are traces that reach the end*) +lemma "\NB. \evs \ woolam. + Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) \ set evs" +apply (intro exI bexI) +apply (rule_tac [2] woolam.Nil + [THEN woolam.WL1, THEN woolam.WL2, THEN woolam.WL3, + THEN woolam.WL4, THEN woolam.WL5]) +apply possibility +done + +(*Could prove forwarding lemmas for WL4, but we do not need them!*) + +(**** Inductive proofs about woolam ****) + +(** Theorems of the form X \ parts (spies evs) imply that NOBODY + sends messages containing X! **) + +(*Spy never sees a good agent's shared key!*) +lemma Spy_see_shrK [simp]: + "evs \ woolam ==> (Key (shrK A) \ parts (spies evs)) = (A \ bad)" +apply (erule woolam.induct, force, simp_all) +apply blast+ +done + +lemma Spy_analz_shrK [simp]: + "evs \ woolam ==> (Key (shrK A) \ analz (spies evs)) = (A \ bad)" +by auto + +lemma Spy_see_shrK_D [dest!]: + "[|Key (shrK A) \ parts (knows Spy evs); evs \ woolam|] ==> A \ bad" +by (blast dest: Spy_see_shrK) + + +(**** Autheticity properties for Woo-Lam ****) + +(*** WL4 ***) + +(*If the encrypted message appears then it originated with Alice*) +lemma NB_Crypt_imp_Alice_msg: + "[| Crypt (shrK A) (Nonce NB) \ parts (spies evs); + A \ bad; evs \ woolam |] + ==> \B. Says A B (Crypt (shrK A) (Nonce NB)) \ set evs" +apply (erule rev_mp, erule woolam.induct, force, simp_all) +apply blast+ +done + +(*Guarantee for Server: if it gets a message containing a certificate from + Alice, then she originated that certificate. But we DO NOT know that B + ever saw it: the Spy may have rerouted the message to the Server.*) +lemma Server_trusts_WL4 [dest]: + "[| Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} + \ set evs; + A \ bad; evs \ woolam |] + ==> \B. Says A B (Crypt (shrK A) (Nonce NB)) \ set evs" +by (blast intro!: NB_Crypt_imp_Alice_msg) + + +(*** WL5 ***) + +(*Server sent WL5 only if it received the right sort of message*) +lemma Server_sent_WL5 [dest]: + "[| Says Server B (Crypt (shrK B) {|Agent A, NB|}) \ set evs; + evs \ woolam |] + ==> \B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} + \ set evs" +apply (erule rev_mp, erule woolam.induct, force, simp_all) +apply blast+ +done + +(*If the encrypted message appears then it originated with the Server!*) +lemma NB_Crypt_imp_Server_msg [rule_format]: + "[| Crypt (shrK B) {|Agent A, NB|} \ parts (spies evs); + B \ bad; evs \ woolam |] + ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) \ set evs" +apply (erule rev_mp, erule woolam.induct, force, simp_all) +apply blast+ +done + +(*Guarantee for B. If B gets the Server's certificate then A has encrypted + the nonce using her key. This event can be no older than the nonce itself. + But A may have sent the nonce to some other agent and it could have reached + the Server via the Spy.*) +lemma B_trusts_WL5: + "[| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs; + A \ bad; B \ bad; evs \ woolam |] + ==> \B. Says A B (Crypt (shrK A) (Nonce NB)) \ set evs" +by (blast dest!: NB_Crypt_imp_Server_msg) + + +(*B only issues challenges in response to WL1. Not used.*) +lemma B_said_WL2: + "[| Says B A (Nonce NB) \ set evs; B \ Spy; evs \ woolam |] + ==> \A'. Says A' B (Agent A) \ set evs" +apply (erule rev_mp, erule woolam.induct, force, simp_all) +apply blast+ +done + + +(**CANNOT be proved because A doesn't know where challenges come from...*) +lemma "[| A \ bad; B \ Spy; evs \ woolam |] + ==> Crypt (shrK A) (Nonce NB) \ parts (spies evs) & + Says B A (Nonce NB) \ set evs + --> Says A B (Crypt (shrK A) (Nonce NB)) \ set evs" +apply (erule rev_mp, erule woolam.induct, force, simp_all) +apply blast +apply auto +oops end diff -r c8bbf4c4bc2d -r a6816d47f41d src/HOL/Auth/Yahalom.ML --- a/src/HOL/Auth/Yahalom.ML Wed Apr 11 11:53:54 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,626 +0,0 @@ -(* Title: HOL/Auth/Yahalom - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1996 University of Cambridge - -Inductive relation "yahalom" for the Yahalom protocol. - -From page 257 of - Burrows, Abadi and Needham. A Logic of Authentication. - Proc. Royal Soc. 426 (1989) -*) - -Pretty.setdepth 25; - - -(*A "possibility property": there are traces that reach the end*) -Goal "A \\ Server \ -\ ==> \\X NB K. \\evs \\ yahalom. \ -\ Says A B {|X, Crypt K (Nonce NB)|} \\ set evs"; -by (REPEAT (resolve_tac [exI,bexI] 1)); -by (rtac (yahalom.Nil RS - yahalom.YM1 RS yahalom.Reception RS - yahalom.YM2 RS yahalom.Reception RS - yahalom.YM3 RS yahalom.Reception RS yahalom.YM4) 2); -by possibility_tac; -result(); - -Goal "[| Gets B X \\ set evs; evs \\ yahalom |] ==> \\A. Says A B X \\ set evs"; -by (etac rev_mp 1); -by (etac yahalom.induct 1); -by Auto_tac; -qed "Gets_imp_Says"; - -(*Must be proved separately for each protocol*) -Goal "[| Gets B X \\ set evs; evs \\ yahalom |] ==> X \\ knows Spy evs"; -by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1); -qed"Gets_imp_knows_Spy"; -AddDs [Gets_imp_knows_Spy RS parts.Inj]; - - -(**** Inductive proofs about yahalom ****) - - -(** For reasoning about the encrypted portion of messages **) - -(*Lets us treat YM4 using a similar argument as for the Fake case.*) -Goal "[| Gets A {|Crypt (shrK A) Y, X|} \\ set evs; evs \\ yahalom |] \ -\ ==> X \\ analz (knows Spy evs)"; -by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1); -qed "YM4_analz_knows_Spy"; - -bind_thm ("YM4_parts_knows_Spy", - YM4_analz_knows_Spy RS (impOfSubs analz_subset_parts)); - -(*For Oops*) -Goal "Says Server A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} \\ set evs \ -\ ==> K \\ parts (knows Spy evs)"; -by (blast_tac (claset() addSDs [parts.Body, - Says_imp_knows_Spy RS parts.Inj]) 1); -qed "YM4_Key_parts_knows_Spy"; - -(*For proving the easier theorems about X \\ parts (knows Spy evs).*) -fun parts_knows_Spy_tac i = - EVERY - [ftac YM4_Key_parts_knows_Spy (i+7), - ftac YM4_parts_knows_Spy (i+6), assume_tac (i+6), - prove_simple_subgoals_tac i]; - -(*Induction for regularity theorems. If induction formula has the form - X \\ analz (knows Spy evs) --> ... then it shortens the proof by discarding - needless information about analz (insert X (knows Spy evs)) *) -fun parts_induct_tac i = - etac yahalom.induct i - THEN - REPEAT (FIRSTGOAL analz_mono_contra_tac) - THEN parts_knows_Spy_tac i; - - -(** Theorems of the form X \\ parts (knows Spy evs) imply that NOBODY - sends messages containing X! **) - -(*Spy never sees another agent's shared key! (unless it's bad at start)*) -Goal "evs \\ yahalom ==> (Key (shrK A) \\ parts (knows Spy evs)) = (A \\ bad)"; -by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); -by (ALLGOALS Blast_tac); -qed "Spy_see_shrK"; -Addsimps [Spy_see_shrK]; - -Goal "evs \\ yahalom ==> (Key (shrK A) \\ analz (knows Spy evs)) = (A \\ bad)"; -by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); -qed "Spy_analz_shrK"; -Addsimps [Spy_analz_shrK]; - -AddSDs [Spy_see_shrK RSN (2, rev_iffD1), - Spy_analz_shrK RSN (2, rev_iffD1)]; - - -(*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*) -Goal "evs \\ yahalom ==> \ -\ Key K \\ used evs --> K \\ keysFor (parts (knows Spy evs))"; -by (parts_induct_tac 1); -(*Fake*) -by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); -(*YM2-4: Because Key K is not fresh, etc.*) -by (REPEAT (blast_tac (claset() addSEs knows_Spy_partsEs) 1)); -qed_spec_mp "new_keys_not_used"; -Addsimps [new_keys_not_used]; - -(*Earlier, all protocol proofs declared this theorem. - But few of them actually need it! (Another is Kerberos IV) *) -bind_thm ("new_keys_not_analzd", - [analz_subset_parts RS keysFor_mono, - new_keys_not_used] MRS contra_subsetD); - - -(*Describes the form of K when the Server sends this message. Useful for - Oops as well as main secrecy property.*) -Goal "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \ -\ \\ set evs; evs \\ yahalom |] \ -\ ==> K \\ range shrK"; -by (etac rev_mp 1); -by (etac yahalom.induct 1); -by (ALLGOALS Asm_simp_tac); -by (Blast_tac 1); -qed "Says_Server_not_range"; - -Addsimps [Says_Server_not_range]; - - -(*For proofs involving analz.*) -val analz_knows_Spy_tac = - ftac YM4_analz_knows_Spy 7 THEN assume_tac 7; - -(**** - The following is to prove theorems of the form - - Key K \\ analz (insert (Key KAB) (knows Spy evs)) ==> - Key K \\ analz (knows Spy evs) - - A more general formula must be proved inductively. -****) - -(** Session keys are not used to encrypt other session keys **) - -Goal "evs \\ yahalom ==> \ -\ \\K KK. KK <= - (range shrK) --> \ -\ (Key K \\ analz (Key`KK Un (knows Spy evs))) = \ -\ (K \\ KK | Key K \\ analz (knows Spy evs))"; -by (etac yahalom.induct 1); -by analz_knows_Spy_tac; -by (REPEAT_FIRST (resolve_tac [allI, impI])); -by (REPEAT_FIRST (rtac analz_image_freshK_lemma)); -by (ALLGOALS (asm_simp_tac - (analz_image_freshK_ss addsimps [Says_Server_not_range]))); -(*Fake*) -by (spy_analz_tac 1); -qed_spec_mp "analz_image_freshK"; - -Goal "[| evs \\ yahalom; KAB \\ range shrK |] \ -\ ==> Key K \\ analz (insert (Key KAB) (knows Spy evs)) = \ -\ (K = KAB | Key K \\ analz (knows Spy evs))"; -by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); -qed "analz_insert_freshK"; - - -(*** The Key K uniquely identifies the Server's message. **) - - -Goal "[| Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \\ set evs; \ -\ Says Server A' \ -\ {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} \\ set evs; \ -\ evs \\ yahalom |] \ -\ ==> A=A' & B=B' & na=na' & nb=nb'"; -by (etac rev_mp 1); -by (etac rev_mp 1); -by (etac yahalom.induct 1); -by (ALLGOALS Asm_simp_tac); -(*YM4*) -by (Blast_tac 2); -(*YM3, by freshness*) -by (blast_tac (claset() addSEs knows_Spy_partsEs) 1); -qed "unique_session_keys"; - - -(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **) - -Goal "[| A \\ bad; B \\ bad; evs \\ yahalom |] \ -\ ==> Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \ -\ Crypt (shrK B) {|Agent A, Key K|}|} \ -\ \\ set evs --> \ -\ Notes Spy {|na, nb, Key K|} \\ set evs --> \ -\ Key K \\ analz (knows Spy evs)"; -by (etac yahalom.induct 1); -by analz_knows_Spy_tac; -by (ALLGOALS - (asm_simp_tac - (simpset() addsimps split_ifs @ pushes @ - [analz_insert_eq, analz_insert_freshK]))); -(*Oops*) -by (blast_tac (claset() addDs [unique_session_keys]) 3); -(*YM3*) -by (blast_tac (claset() delrules [impCE] - addSEs knows_Spy_partsEs - addIs [impOfSubs analz_subset_parts]) 2); -(*Fake*) -by (spy_analz_tac 1); -val lemma = result() RS mp RS mp RSN(2,rev_notE); - - -(*Final version*) -Goal "[| Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \ -\ Crypt (shrK B) {|Agent A, Key K|}|} \ -\ \\ set evs; \ -\ Notes Spy {|na, nb, Key K|} \\ set evs; \ -\ A \\ bad; B \\ bad; evs \\ yahalom |] \ -\ ==> Key K \\ analz (knows Spy evs)"; -by (blast_tac (claset() addSEs [lemma]) 1); -qed "Spy_not_see_encrypted_key"; - - -(** Security Guarantee for A upon receiving YM3 **) - -(*If the encrypted message appears then it originated with the Server*) -Goal "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \\ parts (knows Spy evs); \ -\ A \\ bad; evs \\ yahalom |] \ -\ ==> Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \ -\ Crypt (shrK B) {|Agent A, Key K|}|} \ -\ \\ set evs"; -by (etac rev_mp 1); -by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); -qed "A_trusts_YM3"; - -(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*) -Goal "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \\ parts (knows Spy evs); \ -\ Notes Spy {|na, nb, Key K|} \\ set evs; \ -\ A \\ bad; B \\ bad; evs \\ yahalom |] \ -\ ==> Key K \\ analz (knows Spy evs)"; -by (blast_tac (claset() addSDs [A_trusts_YM3, Spy_not_see_encrypted_key]) 1); -qed "A_gets_good_key"; - -(** Security Guarantees for B upon receiving YM4 **) - -(*B knows, by the first part of A's message, that the Server distributed - the key for A and B. But this part says nothing about nonces.*) -Goal "[| Crypt (shrK B) {|Agent A, Key K|} \\ parts (knows Spy evs); \ -\ B \\ bad; evs \\ yahalom |] \ -\ ==> \\NA NB. Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, \ -\ Nonce NA, Nonce NB|}, \ -\ Crypt (shrK B) {|Agent A, Key K|}|} \ -\ \\ set evs"; -by (etac rev_mp 1); -by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); -(*YM3*) -by (Blast_tac 1); -qed "B_trusts_YM4_shrK"; - -(*B knows, by the second part of A's message, that the Server distributed - the key quoting nonce NB. This part says nothing about agent names. - Secrecy of NB is crucial. Note that Nonce NB \\ analz(knows Spy evs) must - be the FIRST antecedent of the induction formula.*) -Goal "evs \\ yahalom \ -\ ==> Nonce NB \\ analz (knows Spy evs) --> \ -\ Crypt K (Nonce NB) \\ parts (knows Spy evs) --> \ -\ (\\A B NA. Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, \ -\ Nonce NA, Nonce NB|}, \ -\ Crypt (shrK B) {|Agent A, Key K|}|} \ -\ \\ set evs)"; -by (parts_induct_tac 1); -by (ALLGOALS Clarify_tac); -(*YM3 & Fake*) -by (Blast_tac 2); -by (Fake_parts_insert_tac 1); -(*YM4*) -(*A is uncompromised because NB is secure; - A's certificate guarantees the existence of the Server message*) -by (blast_tac (claset() addSDs [Gets_imp_Says, Crypt_Spy_analz_bad] - addDs [Says_imp_spies, analz.Inj, - parts.Inj RS parts.Fst RS A_trusts_YM3]) 1); -bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp)); - - -(**** Towards proving secrecy of Nonce NB ****) - -(** Lemmas about the predicate KeyWithNonce **) - -Goalw [KeyWithNonce_def] - "Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \ -\ \\ set evs ==> KeyWithNonce K NB evs"; -by (Blast_tac 1); -qed "KeyWithNonceI"; - -Goalw [KeyWithNonce_def] - "KeyWithNonce K NB (Says S A X # evs) = \ -\ (Server = S & \ -\ (\\B n X'. X = {|Crypt (shrK A) {|Agent B, Key K, n, Nonce NB|}, X'|}) \ -\ | KeyWithNonce K NB evs)"; -by (Simp_tac 1); -by (Blast_tac 1); -qed "KeyWithNonce_Says"; -Addsimps [KeyWithNonce_Says]; - -Goalw [KeyWithNonce_def] - "KeyWithNonce K NB (Notes A X # evs) = KeyWithNonce K NB evs"; -by (Simp_tac 1); -qed "KeyWithNonce_Notes"; -Addsimps [KeyWithNonce_Notes]; - -Goalw [KeyWithNonce_def] - "KeyWithNonce K NB (Gets A X # evs) = KeyWithNonce K NB evs"; -by (Simp_tac 1); -qed "KeyWithNonce_Gets"; -Addsimps [KeyWithNonce_Gets]; - -(*A fresh key cannot be associated with any nonce - (with respect to a given trace). *) -Goalw [KeyWithNonce_def] - "Key K \\ used evs ==> ~ KeyWithNonce K NB evs"; -by (blast_tac (claset() addSEs knows_Spy_partsEs) 1); -qed "fresh_not_KeyWithNonce"; - -(*The Server message associates K with NB' and therefore not with any - other nonce NB.*) -Goalw [KeyWithNonce_def] - "[| Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|} \ -\ \\ set evs; \ -\ NB \\ NB'; evs \\ yahalom |] \ -\ ==> ~ KeyWithNonce K NB evs"; -by (blast_tac (claset() addDs [unique_session_keys]) 1); -qed "Says_Server_KeyWithNonce"; - - -(*The only nonces that can be found with the help of session keys are - those distributed as nonce NB by the Server. The form of the theorem - recalls analz_image_freshK, but it is much more complicated.*) - - -(*As with analz_image_freshK, we take some pains to express the property - as a logical equivalence so that the simplifier can apply it.*) -Goal "P --> (X \\ analz (G Un H)) --> (X \\ analz H) ==> \ -\ P --> (X \\ analz (G Un H)) = (X \\ analz H)"; -by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1); -val Nonce_secrecy_lemma = result(); - -Goal "evs \\ yahalom ==> \ -\ (\\KK. KK <= - (range shrK) --> \ -\ (\\K \\ KK. ~ KeyWithNonce K NB evs) --> \ -\ (Nonce NB \\ analz (Key`KK Un (knows Spy evs))) = \ -\ (Nonce NB \\ analz (knows Spy evs)))"; -by (etac yahalom.induct 1); -by analz_knows_Spy_tac; -by (REPEAT_FIRST (resolve_tac [impI RS allI])); -by (REPEAT_FIRST (rtac Nonce_secrecy_lemma)); -(*For Oops, simplification proves NBa\\NB. By Says_Server_KeyWithNonce, - we get (~ KeyWithNonce K NB evs); then simplification can apply the - induction hypothesis with KK = {K}.*) -by (ALLGOALS (*4 seconds*) - (asm_simp_tac - (analz_image_freshK_ss - addsimps split_ifs - addsimps [all_conj_distrib, ball_conj_distrib, analz_image_freshK, - KeyWithNonce_Says, KeyWithNonce_Notes, KeyWithNonce_Gets, - fresh_not_KeyWithNonce, Says_Server_not_range, - imp_disj_not1, (*Moves NBa\\NB to the front*) - Says_Server_KeyWithNonce]))); -(*Fake*) -by (spy_analz_tac 1); -(*YM4*) (** LEVEL 6 **) -by (thin_tac "\\KK. ?P KK" 1); -by (Clarify_tac 1); -(*If A:bad then NBa is known, therefore NBa \\ NB. Previous two steps make - the next step faster.*) -by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_spies, - Crypt_Spy_analz_bad] - addDs [analz.Inj, - parts.Inj RS parts.Fst RS A_trusts_YM3 RS KeyWithNonceI]) 1); -qed_spec_mp "Nonce_secrecy"; - - -(*Version required below: if NB can be decrypted using a session key then it - was distributed with that key. The more general form above is required - for the induction to carry through.*) -Goal "[| Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|} \ -\ \\ set evs; \ -\ NB \\ NB'; KAB \\ range shrK; evs \\ yahalom |] \ -\ ==> (Nonce NB \\ analz (insert (Key KAB) (knows Spy evs))) = \ -\ (Nonce NB \\ analz (knows Spy evs))"; -by (asm_simp_tac (analz_image_freshK_ss addsimps - [Nonce_secrecy, Says_Server_KeyWithNonce]) 1); -qed "single_Nonce_secrecy"; - - -(*** The Nonce NB uniquely identifies B's message. ***) - -Goal "[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} \\ parts (knows Spy evs); \ -\ Crypt (shrK B') {|Agent A', Nonce NA', nb|} \\ parts (knows Spy evs); \ -\ evs \\ yahalom; B \\ bad; B' \\ bad |] \ -\ ==> NA' = NA & A' = A & B' = B"; -by (etac rev_mp 1); -by (etac rev_mp 1); -by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); -(*YM2, by freshness*) -by (blast_tac (claset() addSEs knows_Spy_partsEs) 1); -qed "unique_NB"; - - -(*Variant useful for proving secrecy of NB. Because nb is assumed to be - secret, we no longer must assume B, B' not bad.*) -Goal "[| Says C S {|X, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \ -\ \\ set evs; \ -\ Gets S' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|} \ -\ \\ set evs; \ -\ nb \\ analz (knows Spy evs); evs \\ yahalom |] \ -\ ==> NA' = NA & A' = A & B' = B"; -by (blast_tac (claset() addSDs [Gets_imp_Says, Crypt_Spy_analz_bad] - addDs [Says_imp_spies, unique_NB, parts.Inj, - analz.Inj]) 1); -qed "Says_unique_NB"; - - -(** A nonce value is never used both as NA and as NB **) - -Goal "evs \\ yahalom \ -\ ==> Nonce NB \\ analz (knows Spy evs) --> \ -\ Crypt (shrK B') {|Agent A', Nonce NB, nb'|} \\ parts(knows Spy evs) --> \ -\ Crypt (shrK B) {|Agent A, na, Nonce NB|} \\ parts(knows Spy evs)"; -by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); -by (blast_tac (claset() addDs [Gets_imp_knows_Spy RS analz.Inj] - addSIs [parts_insertI] - addSDs [parts.Body]) 1); -bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE)); - -(*more readable version cited in Yahalom paper*) -standard (result() RS mp RSN (2,rev_mp)); - -(*The Server sends YM3 only in response to YM2.*) -Goal "[| Says Server A \ -\ {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} \\ set evs; \ -\ evs \\ yahalom |] \ -\ ==> Gets Server {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \ -\ \\ set evs"; -by (etac rev_mp 1); -by (etac yahalom.induct 1); -by Auto_tac; -qed "Says_Server_imp_YM2"; - - -(*A vital theorem for B, that nonce NB remains secure from the Spy.*) -Goal "[| A \\ bad; B \\ bad; evs \\ yahalom |] \ -\ ==> (\\k. Notes Spy {|Nonce NA, Nonce NB, k|} \\ set evs) --> \ -\ Says B Server \ -\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \ -\ \\ set evs --> \ -\ Nonce NB \\ analz (knows Spy evs)"; -by (etac yahalom.induct 1); -by analz_knows_Spy_tac; -by (ALLGOALS - (asm_simp_tac - (simpset() addsimps split_ifs @ pushes @ - [new_keys_not_analzd, analz_insert_eq, analz_insert_freshK]))); -(*Prove YM3 by showing that no NB can also be an NA*) -by (blast_tac (claset() addDs [Says_imp_knows_Spy RS parts.Inj] - addSEs [no_nonce_YM1_YM2, MPair_parts] - addDs [Gets_imp_Says, Says_unique_NB]) 4); -(*YM2: similar freshness reasoning*) -by (blast_tac (claset() addSDs [parts.Body] - addDs [Gets_imp_Says, - Says_imp_knows_Spy RS analz.Inj, - impOfSubs analz_subset_parts]) 3); -(*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*) -by (blast_tac (claset() addSIs [parts_insertI] - addSEs knows_Spy_partsEs) 2); -(*Fake*) -by (spy_analz_tac 1); -(** LEVEL 7: YM4 and Oops remain **) -by (ALLGOALS (Clarify_tac THEN' - full_simp_tac (simpset() addsimps [all_conj_distrib]))); -(*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) -(*Case analysis on Aa:bad; PROOF FAILED problems; - use Says_unique_NB to identify message components: Aa=A, Ba=B*) -by (blast_tac (claset() addSDs [Says_unique_NB, - parts.Inj RS parts.Fst RS A_trusts_YM3] - addDs [Gets_imp_knows_Spy RS analz.Inj, Gets_imp_Says, - Says_imp_spies, Says_Server_imp_YM2, - Spy_not_see_encrypted_key]) 1); -(** LEVEL 9 **) -(*Oops case: if the nonce is betrayed now, show that the Oops event is - covered by the quantified Oops assumption.*) -by (ftac Says_Server_imp_YM2 1 THEN assume_tac 1); -by (case_tac "NB = NBa" 1); -(*If NB=NBa then all other components of the Oops message agree*) -by (blast_tac (claset() addDs [Says_unique_NB]) 1); -(*case NB \\ NBa*) -by (asm_simp_tac (simpset() addsimps [single_Nonce_secrecy]) 1); -by (blast_tac (claset() addSEs [no_nonce_YM1_YM2] (*to prove NB\\NAa*) - addDs [Says_imp_knows_Spy RS parts.Inj]) 1); -bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp)); - - -(*B's session key guarantee from YM4. The two certificates contribute to a - single conclusion about the Server's message. Note that the "Notes Spy" - assumption must quantify over \\POSSIBLE keys instead of our particular K. - If this run is broken and the spy substitutes a certificate containing an - old key, B has no means of telling.*) -Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, \ -\ Crypt K (Nonce NB)|} \\ set evs; \ -\ Says B Server \ -\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \ -\ \\ set evs; \ -\ \\k. Notes Spy {|Nonce NA, Nonce NB, k|} \\ set evs; \ -\ A \\ bad; B \\ bad; evs \\ yahalom |] \ -\ ==> Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, \ -\ Nonce NA, Nonce NB|}, \ -\ Crypt (shrK B) {|Agent A, Key K|}|} \ -\ \\ set evs"; -by (blast_tac (claset() addDs [Spy_not_see_NB, Says_unique_NB, - Says_Server_imp_YM2, B_trusts_YM4_newK]) 1); -qed "B_trusts_YM4"; - - -(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*) -Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, \ -\ Crypt K (Nonce NB)|} \\ set evs; \ -\ Says B Server \ -\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \ -\ \\ set evs; \ -\ \\k. Notes Spy {|Nonce NA, Nonce NB, k|} \\ set evs; \ -\ A \\ bad; B \\ bad; evs \\ yahalom |] \ -\ ==> Key K \\ analz (knows Spy evs)"; -by (blast_tac (claset() addSDs [B_trusts_YM4, Spy_not_see_encrypted_key]) 1); -qed "B_gets_good_key"; - - -(*** Authenticating B to A ***) - -(*The encryption in message YM2 tells us it cannot be faked.*) -Goal "evs \\ yahalom \ -\ ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|} \\ parts (knows Spy evs) --> \ -\ B \\ bad --> \ -\ Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \ -\ \\ set evs"; -by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); -bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp); - -(*If the server sends YM3 then B sent YM2*) -Goal "evs \\ yahalom \ -\ ==> Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \ -\ \\ set evs --> \ -\ B \\ bad --> \ -\ Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \ -\ \\ set evs"; -by (etac yahalom.induct 1); -by (ALLGOALS Asm_simp_tac); -(*YM4*) -by (Blast_tac 2); -(*YM3*) -by (blast_tac (claset() addSDs [B_Said_YM2, - Says_imp_knows_Spy RS parts.Inj]) 1); -val lemma = result() RSN (2, rev_mp) RS mp |> standard; - -(*If A receives YM3 then B has used nonce NA (and therefore is alive)*) -Goal "[| Gets A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \ -\ \\ set evs; \ -\ A \\ bad; B \\ bad; evs \\ yahalom |] \ -\==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \ -\ \\ set evs"; -by (blast_tac (claset() addSDs [A_trusts_YM3, lemma] - addEs knows_Spy_partsEs) 1); -qed "YM3_auth_B_to_A"; - - -(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***) - -(*Assuming the session key is secure, if both certificates are present then - A has said NB. We can't be sure about the rest of A's message, but only - NB matters for freshness.*) -Goal "evs \\ yahalom \ -\ ==> Key K \\ analz (knows Spy evs) --> \ -\ Crypt K (Nonce NB) \\ parts (knows Spy evs) --> \ -\ Crypt (shrK B) {|Agent A, Key K|} \\ parts (knows Spy evs) --> \ -\ B \\ bad --> \ -\ (\\X. Says A B {|X, Crypt K (Nonce NB)|} \\ set evs)"; -by (parts_induct_tac 1); -(*Fake*) -by (Fake_parts_insert_tac 1); -(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*) -by (fast_tac (claset() addSDs [Crypt_imp_keysFor] addss (simpset())) 1); -(*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*) -by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1); -(*yes: apply unicity of session keys*) -by (blast_tac (claset() addSDs [Gets_imp_Says, A_trusts_YM3, B_trusts_YM4_shrK, - Crypt_Spy_analz_bad] - addDs [Says_imp_knows_Spy RS parts.Inj, - Says_imp_spies RS analz.Inj, unique_session_keys]) 1); -qed_spec_mp "A_Said_YM3_lemma"; - -(*If B receives YM4 then A has used nonce NB (and therefore is alive). - Moreover, A associates K with NB (thus is talking about the same run). - Other premises guarantee secrecy of K.*) -Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, \ -\ Crypt K (Nonce NB)|} \\ set evs; \ -\ Says B Server \ -\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \ -\ \\ set evs; \ -\ (\\NA k. Notes Spy {|Nonce NA, Nonce NB, k|} \\ set evs); \ -\ A \\ bad; B \\ bad; evs \\ yahalom |] \ -\ ==> \\X. Says A B {|X, Crypt K (Nonce NB)|} \\ set evs"; -by (blast_tac (claset() addSIs [A_Said_YM3_lemma] - addDs [Spy_not_see_encrypted_key, B_trusts_YM4, - Gets_imp_Says, Says_imp_knows_Spy RS parts.Inj]) 1); -qed_spec_mp "YM4_imp_A_Said_YM3"; diff -r c8bbf4c4bc2d -r a6816d47f41d src/HOL/Auth/Yahalom.thy --- a/src/HOL/Auth/Yahalom.thy Wed Apr 11 11:53:54 2001 +0200 +++ b/src/HOL/Auth/Yahalom.thy Thu Apr 12 12:45:05 2001 +0200 @@ -8,73 +8,633 @@ From page 257 of Burrows, Abadi and Needham. A Logic of Authentication. Proc. Royal Soc. 426 (1989) + +This theory has the prototypical example of a secrecy relation, KeyCryptNonce. *) -Yahalom = Shared + +theory Yahalom = Shared: -consts yahalom :: event list set +consts yahalom :: "event list set" inductive "yahalom" - intrs + intros (*Initial trace is empty*) - Nil "[] \\ yahalom" + Nil: "[] \ yahalom" (*The spy MAY say anything he CAN say. We do not expect him to invent new nonces here, but he can also use NS1. Common to all similar protocols.*) - Fake "[| evsf \\ yahalom; X \\ synth (analz (knows Spy evsf)) |] - ==> Says Spy B X # evsf \\ yahalom" + Fake: "[| evsf \ yahalom; X \ synth (analz (knows Spy evsf)) |] + ==> Says Spy B X # evsf \ yahalom" (*A message that has been sent can be received by the intended recipient.*) - Reception "[| evsr \\ yahalom; Says A B X \\ set evsr |] - ==> Gets B X # evsr \\ yahalom" + Reception: "[| evsr \ yahalom; Says A B X \ set evsr |] + ==> Gets B X # evsr \ yahalom" (*Alice initiates a protocol run*) - YM1 "[| evs1 \\ yahalom; Nonce NA \\ used evs1 |] - ==> Says A B {|Agent A, Nonce NA|} # evs1 \\ yahalom" + YM1: "[| evs1 \ yahalom; Nonce NA \ used evs1 |] + ==> Says A B {|Agent A, Nonce NA|} # evs1 \ yahalom" (*Bob's response to Alice's message.*) - YM2 "[| evs2 \\ yahalom; Nonce NB \\ used evs2; - Gets B {|Agent A, Nonce NA|} \\ set evs2 |] + YM2: "[| evs2 \ yahalom; Nonce NB \ used evs2; + Gets B {|Agent A, Nonce NA|} \ set evs2 |] ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} - # evs2 \\ yahalom" + # evs2 \ yahalom" (*The Server receives Bob's message. He responds by sending a new session key to Alice, with a packet for forwarding to Bob.*) - YM3 "[| evs3 \\ yahalom; Key KAB \\ used evs3; + YM3: "[| evs3 \ yahalom; Key KAB \ used evs3; Gets Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} - \\ set evs3 |] + \ set evs3 |] ==> Says Server A {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|}, Crypt (shrK B) {|Agent A, Key KAB|}|} - # evs3 \\ yahalom" + # evs3 \ yahalom" (*Alice receives the Server's (?) message, checks her Nonce, and uses the new session key to send Bob his Nonce. The premise - A \\ Server is needed to prove Says_Server_not_range.*) - YM4 "[| evs4 \\ yahalom; A \\ Server; + A \ Server is needed to prove Says_Server_not_range.*) + YM4: "[| evs4 \ yahalom; A \ Server; Gets A {|Crypt(shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|} - \\ set evs4; - Says A B {|Agent A, Nonce NA|} \\ set evs4 |] - ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \\ yahalom" + \ set evs4; + Says A B {|Agent A, Nonce NA|} \ set evs4 |] + ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \ yahalom" (*This message models possible leaks of session keys. The Nonces identify the protocol run. Quoting Server here ensures they are correct.*) - Oops "[| evso \\ yahalom; + Oops: "[| evso \ yahalom; Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, - X|} \\ set evso |] - ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \\ yahalom" + X|} \ set evso |] + ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \ yahalom" constdefs - KeyWithNonce :: [key, nat, event list] => bool + KeyWithNonce :: "[key, nat, event list] => bool" "KeyWithNonce K NB evs == - \\A B na X. + \A B na X. Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} - \\ set evs" + \ set evs" + + +declare Says_imp_knows_Spy [THEN analz.Inj, dest] +declare parts.Body [dest] +declare Fake_parts_insert_in_Un [dest] +declare analz_into_parts [dest] + +(*A "possibility property": there are traces that reach the end*) +lemma "A \ Server + ==> \X NB K. \evs \ yahalom. + Says A B {|X, Crypt K (Nonce NB)|} \ set evs" +apply (intro exI bexI) +apply (rule_tac [2] yahalom.Nil + [THEN yahalom.YM1, THEN yahalom.Reception, + THEN yahalom.YM2, THEN yahalom.Reception, + THEN yahalom.YM3, THEN yahalom.Reception, + THEN yahalom.YM4]) +apply possibility +done + +lemma Gets_imp_Says: + "[| Gets B X \ set evs; evs \ yahalom |] ==> \A. Says A B X \ set evs" +by (erule rev_mp, erule yahalom.induct, auto) + +(*Must be proved separately for each protocol*) +lemma Gets_imp_knows_Spy: + "[| Gets B X \ set evs; evs \ yahalom |] ==> X \ knows Spy evs" +by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) + +declare Gets_imp_knows_Spy [THEN analz.Inj, dest] + + +(**** Inductive proofs about yahalom ****) + +(*Lets us treat YM4 using a similar argument as for the Fake case.*) +lemma YM4_analz_knows_Spy: + "[| Gets A {|Crypt (shrK A) Y, X|} \ set evs; evs \ yahalom |] + ==> X \ analz (knows Spy evs)" +by blast + +lemmas YM4_parts_knows_Spy = + YM4_analz_knows_Spy [THEN analz_into_parts, standard] + +(*For Oops*) +lemma YM4_Key_parts_knows_Spy: + "Says Server A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} \ set evs + ==> K \ parts (knows Spy evs)" +by (blast dest!: parts.Body Says_imp_knows_Spy [THEN parts.Inj]) + + +(** Theorems of the form X \ parts (knows Spy evs) imply that NOBODY + sends messages containing X! **) + +(*Spy never sees a good agent's shared key!*) +lemma Spy_see_shrK [simp]: + "evs \ yahalom ==> (Key (shrK A) \ parts (knows Spy evs)) = (A \ bad)" +apply (erule yahalom.induct, force, + drule_tac [6] YM4_parts_knows_Spy, simp_all) +apply blast+ +done + +lemma Spy_analz_shrK [simp]: + "evs \ yahalom ==> (Key (shrK A) \ analz (knows Spy evs)) = (A \ bad)" +by auto + +lemma Spy_see_shrK_D [dest!]: + "[|Key (shrK A) \ parts (knows Spy evs); evs \ yahalom|] ==> A \ bad" +by (blast dest: Spy_see_shrK) + +(*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*) +lemma new_keys_not_used [rule_format, simp]: + "evs \ yahalom ==> Key K \ used evs --> K \ keysFor (parts (knows Spy evs))" +apply (erule yahalom.induct, force, + frule_tac [6] YM4_parts_knows_Spy, simp_all) +(*Fake, YM3, YM4*) +apply (blast dest!: keysFor_parts_insert)+ +done + + +(*Earlier, all protocol proofs declared this theorem. + But only a few proofs need it, e.g. Yahalom and Kerberos IV.*) +lemma new_keys_not_analzd: + "[|evs \ yahalom; Key K \ used evs|] ==> K \ keysFor (analz (knows Spy evs))" +by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD]) + + +(*Describes the form of K when the Server sends this message. Useful for + Oops as well as main secrecy property.*) +lemma Says_Server_not_range [simp]: + "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} + \ set evs; evs \ yahalom |] + ==> K \ range shrK" +apply (erule rev_mp, erule yahalom.induct, simp_all) +apply blast +done + + +(*For proofs involving analz. +val analz_knows_Spy_tac = + ftac YM4_analz_knows_Spy 7 THEN assume_tac 7 +*) + +(**** + The following is to prove theorems of the form + + Key K \ analz (insert (Key KAB) (knows Spy evs)) ==> + Key K \ analz (knows Spy evs) + + A more general formula must be proved inductively. +****) + +(** Session keys are not used to encrypt other session keys **) + +lemma analz_image_freshK [rule_format]: + "evs \ yahalom ==> + \K KK. KK <= - (range shrK) --> + (Key K \ analz (Key`KK Un (knows Spy evs))) = + (K \ KK | Key K \ analz (knows Spy evs))" +apply (erule yahalom.induct, force, + drule_tac [6] YM4_analz_knows_Spy) +apply analz_freshK +apply spy_analz +apply (simp only: Says_Server_not_range analz_image_freshK_simps) +done + +lemma analz_insert_freshK: + "[| evs \ yahalom; KAB \ range shrK |] ==> + Key K \ analz (insert (Key KAB) (knows Spy evs)) = + (K = KAB | Key K \ analz (knows Spy evs))" +by (simp only: analz_image_freshK analz_image_freshK_simps) + + +(*** The Key K uniquely identifies the Server's message. **) + +lemma unique_session_keys: + "[| Says Server A + {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \ set evs; + Says Server A' + {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} \ set evs; + evs \ yahalom |] + ==> A=A' & B=B' & na=na' & nb=nb'" +apply (erule rev_mp, erule rev_mp) +apply (erule yahalom.induct, simp_all) +(*YM3, by freshness, and YM4*) +apply blast+ +done + + +(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **) + +lemma secrecy_lemma: + "[| A \ bad; B \ bad; evs \ yahalom |] + ==> Says Server A + {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, + Crypt (shrK B) {|Agent A, Key K|}|} + \ set evs --> + Notes Spy {|na, nb, Key K|} \ set evs --> + Key K \ analz (knows Spy evs)" +apply (erule yahalom.induct, force, + drule_tac [6] YM4_analz_knows_Spy) +apply (simp_all add: pushes analz_insert_eq analz_insert_freshK) +apply spy_analz (*Fake*) +apply (blast dest: unique_session_keys)+ (*YM3, Oops*) +done + +(*Final version*) +lemma Spy_not_see_encrypted_key: + "[| Says Server A + {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, + Crypt (shrK B) {|Agent A, Key K|}|} + \ set evs; + Notes Spy {|na, nb, Key K|} \ set evs; + A \ bad; B \ bad; evs \ yahalom |] + ==> Key K \ analz (knows Spy evs)" +by (blast dest: secrecy_lemma) + + +(** Security Guarantee for A upon receiving YM3 **) + +(*If the encrypted message appears then it originated with the Server*) +lemma A_trusts_YM3: + "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \ parts (knows Spy evs); + A \ bad; evs \ yahalom |] + ==> Says Server A + {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, + Crypt (shrK B) {|Agent A, Key K|}|} + \ set evs" +apply (erule rev_mp) +apply (erule yahalom.induct, force, + frule_tac [6] YM4_parts_knows_Spy, simp_all) +(*Fake, YM3*) +apply blast+ +done + +(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*) +lemma A_gets_good_key: + "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \ parts (knows Spy evs); + Notes Spy {|na, nb, Key K|} \ set evs; + A \ bad; B \ bad; evs \ yahalom |] + ==> Key K \ analz (knows Spy evs)" +by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key) + +(** Security Guarantees for B upon receiving YM4 **) + +(*B knows, by the first part of A's message, that the Server distributed + the key for A and B. But this part says nothing about nonces.*) +lemma B_trusts_YM4_shrK: + "[| Crypt (shrK B) {|Agent A, Key K|} \ parts (knows Spy evs); + B \ bad; evs \ yahalom |] + ==> \NA NB. Says Server A + {|Crypt (shrK A) {|Agent B, Key K, + Nonce NA, Nonce NB|}, + Crypt (shrK B) {|Agent A, Key K|}|} + \ set evs" +apply (erule rev_mp) +apply (erule yahalom.induct, force, + frule_tac [6] YM4_parts_knows_Spy, simp_all) +(*Fake, YM3*) +apply blast+ +done + +(*B knows, by the second part of A's message, that the Server distributed + the key quoting nonce NB. This part says nothing about agent names. + Secrecy of NB is crucial. Note that Nonce NB \ analz(knows Spy evs) must + be the FIRST antecedent of the induction formula.*) +lemma B_trusts_YM4_newK[rule_format]: + "[|Crypt K (Nonce NB) \ parts (knows Spy evs); + Nonce NB \ analz (knows Spy evs); evs \ yahalom|] + ==> \A B NA. Says Server A + {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, + Crypt (shrK B) {|Agent A, Key K|}|} + \ set evs" +apply (erule rev_mp, erule rev_mp) +apply (erule yahalom.induct, force, + frule_tac [6] YM4_parts_knows_Spy) +apply (analz_mono_contra, simp_all) +(*Fake, YM3*) +apply blast +apply blast +(*YM4*) +(*A is uncompromised because NB is secure + A's certificate guarantees the existence of the Server message*) +apply (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad + dest: Says_imp_spies + parts.Inj [THEN parts.Fst, THEN A_trusts_YM3]) +done + + +(**** Towards proving secrecy of Nonce NB ****) + +(** Lemmas about the predicate KeyWithNonce **) + +lemma KeyWithNonceI: + "Says Server A + {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} + \ set evs ==> KeyWithNonce K NB evs" +by (unfold KeyWithNonce_def, blast) + +lemma KeyWithNonce_Says [simp]: + "KeyWithNonce K NB (Says S A X # evs) = + (Server = S & + (\B n X'. X = {|Crypt (shrK A) {|Agent B, Key K, n, Nonce NB|}, X'|}) + | KeyWithNonce K NB evs)" +by (simp add: KeyWithNonce_def, blast) + + +lemma KeyWithNonce_Notes [simp]: + "KeyWithNonce K NB (Notes A X # evs) = KeyWithNonce K NB evs" +by (simp add: KeyWithNonce_def) + +lemma KeyWithNonce_Gets [simp]: + "KeyWithNonce K NB (Gets A X # evs) = KeyWithNonce K NB evs" +by (simp add: KeyWithNonce_def) + +(*A fresh key cannot be associated with any nonce + (with respect to a given trace). *) +lemma fresh_not_KeyWithNonce: + "Key K \ used evs ==> ~ KeyWithNonce K NB evs" +by (unfold KeyWithNonce_def, blast) + +(*The Server message associates K with NB' and therefore not with any + other nonce NB.*) +lemma Says_Server_KeyWithNonce: + "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|} + \ set evs; + NB \ NB'; evs \ yahalom |] + ==> ~ KeyWithNonce K NB evs" +by (unfold KeyWithNonce_def, blast dest: unique_session_keys) + + +(*The only nonces that can be found with the help of session keys are + those distributed as nonce NB by the Server. The form of the theorem + recalls analz_image_freshK, but it is much more complicated.*) + + +(*As with analz_image_freshK, we take some pains to express the property + as a logical equivalence so that the simplifier can apply it.*) +lemma Nonce_secrecy_lemma: + "P --> (X \ analz (G Un H)) --> (X \ analz H) ==> + P --> (X \ analz (G Un H)) = (X \ analz H)" +by (blast intro: analz_mono [THEN subsetD]) + +lemma Nonce_secrecy: + "evs \ yahalom ==> + (\KK. KK <= - (range shrK) --> + (\K \ KK. ~ KeyWithNonce K NB evs) --> + (Nonce NB \ analz (Key`KK Un (knows Spy evs))) = + (Nonce NB \ analz (knows Spy evs)))" +apply (erule yahalom.induct, force, + frule_tac [6] YM4_analz_knows_Spy) +apply (safe del: allI impI intro!: Nonce_secrecy_lemma [THEN impI, THEN allI]) +apply (simp_all del: image_insert image_Un + add: analz_image_freshK_simps split_ifs + all_conj_distrib ball_conj_distrib + analz_image_freshK fresh_not_KeyWithNonce + imp_disj_not1 (*Moves NBa\NB to the front*) + Says_Server_KeyWithNonce) +(*For Oops, simplification proves NBa\NB. By Says_Server_KeyWithNonce, + we get (~ KeyWithNonce K NB evs); then simplification can apply the + induction hypothesis with KK = {K}.*) +(*Fake*) +apply spy_analz +(*YM4*) (** LEVEL 6 **) +apply (erule_tac V = "\KK. ?P KK" in thin_rl) +apply clarify +(*If A \ bad then NBa is known, therefore NBa \ NB. Previous two steps make + the next step faster.*) +apply (blast dest!: Gets_imp_Says Says_imp_spies Crypt_Spy_analz_bad + dest: analz.Inj + parts.Inj [THEN parts.Fst, THEN A_trusts_YM3, THEN KeyWithNonceI]) +done + + +(*Version required below: if NB can be decrypted using a session key then it + was distributed with that key. The more general form above is required + for the induction to carry through.*) +lemma single_Nonce_secrecy: + "[| Says Server A + {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|} + \ set evs; + NB \ NB'; KAB \ range shrK; evs \ yahalom |] + ==> (Nonce NB \ analz (insert (Key KAB) (knows Spy evs))) = + (Nonce NB \ analz (knows Spy evs))" +by (simp_all del: image_insert image_Un imp_disjL + add: analz_image_freshK_simps split_ifs + Nonce_secrecy Says_Server_KeyWithNonce); + + +(*** The Nonce NB uniquely identifies B's message. ***) + +lemma unique_NB: + "[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} \ parts (knows Spy evs); + Crypt (shrK B') {|Agent A', Nonce NA', nb|} \ parts (knows Spy evs); + evs \ yahalom; B \ bad; B' \ bad |] + ==> NA' = NA & A' = A & B' = B" +apply (erule rev_mp, erule rev_mp) +apply (erule yahalom.induct, force, + frule_tac [6] YM4_parts_knows_Spy, simp_all) +(*Fake, and YM2 by freshness*) +apply blast+ +done + + +(*Variant useful for proving secrecy of NB. Because nb is assumed to be + secret, we no longer must assume B, B' not bad.*) +lemma Says_unique_NB: + "[| Says C S {|X, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} + \ set evs; + Gets S' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|} + \ set evs; + nb \ analz (knows Spy evs); evs \ yahalom |] + ==> NA' = NA & A' = A & B' = B" +by (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad + dest: Says_imp_spies unique_NB parts.Inj analz.Inj) + + +(** A nonce value is never used both as NA and as NB **) + +lemma no_nonce_YM1_YM2: + "[|Crypt (shrK B') {|Agent A', Nonce NB, nb'|} \ parts(knows Spy evs); + Nonce NB \ analz (knows Spy evs); evs \ yahalom|] + ==> Crypt (shrK B) {|Agent A, na, Nonce NB|} \ parts(knows Spy evs)" +apply (erule rev_mp, erule rev_mp) +apply (erule yahalom.induct, force, + frule_tac [6] YM4_parts_knows_Spy) +apply (analz_mono_contra, simp_all) +(*Fake, YM2*) +apply blast+ +done + +(*The Server sends YM3 only in response to YM2.*) +lemma Says_Server_imp_YM2: + "[| Says Server A {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} \ set evs; + evs \ yahalom |] + ==> Gets Server {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} + \ set evs" +apply (erule rev_mp, erule yahalom.induct) +apply auto +done + + +(*A vital theorem for B, that nonce NB remains secure from the Spy.*) +lemma Spy_not_see_NB : + "[| Says B Server + {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} + \ set evs; + (\k. Notes Spy {|Nonce NA, Nonce NB, k|} \ set evs); + A \ bad; B \ bad; evs \ yahalom |] + ==> Nonce NB \ analz (knows Spy evs)" +apply (erule rev_mp, erule rev_mp) +apply (erule yahalom.induct, force, + frule_tac [6] YM4_analz_knows_Spy) +apply (simp_all add: split_ifs pushes new_keys_not_analzd analz_insert_eq + analz_insert_freshK) +(*Fake*) +apply spy_analz +(*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*) +apply blast +(*YM2*) +apply blast +(*Prove YM3 by showing that no NB can also be an NA*) +apply (blast dest!: no_nonce_YM1_YM2 dest: Gets_imp_Says Says_unique_NB) +(** LEVEL 7: YM4 and Oops remain **) +apply (clarify, simp add: all_conj_distrib) +(*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) +(*Case analysis on Aa:bad; PROOF FAILED problems + use Says_unique_NB to identify message components: Aa=A, Ba=B*) +apply (blast dest!: Says_unique_NB + parts.Inj [THEN parts.Fst, THEN A_trusts_YM3] + dest: Gets_imp_Says Says_imp_spies Says_Server_imp_YM2 + Spy_not_see_encrypted_key) +(*Oops case: if the nonce is betrayed now, show that the Oops event is + covered by the quantified Oops assumption.*) +apply (clarify, simp add: all_conj_distrib) +apply (frule Says_Server_imp_YM2, assumption) +apply (case_tac "NB = NBa") +(*If NB=NBa then all other components of the Oops message agree*) +apply (blast dest: Says_unique_NB) +(*case NB \ NBa*) +apply (simp add: single_Nonce_secrecy) +apply (blast dest!: no_nonce_YM1_YM2 (*to prove NB\NAa*)) +done + + +(*B's session key guarantee from YM4. The two certificates contribute to a + single conclusion about the Server's message. Note that the "Notes Spy" + assumption must quantify over \POSSIBLE keys instead of our particular K. + If this run is broken and the spy substitutes a certificate containing an + old key, B has no means of telling.*) +lemma B_trusts_YM4: + "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, + Crypt K (Nonce NB)|} \ set evs; + Says B Server + {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} + \ set evs; + \k. Notes Spy {|Nonce NA, Nonce NB, k|} \ set evs; + A \ bad; B \ bad; evs \ yahalom |] + ==> Says Server A + {|Crypt (shrK A) {|Agent B, Key K, + Nonce NA, Nonce NB|}, + Crypt (shrK B) {|Agent A, Key K|}|} + \ set evs" +by (blast dest: Spy_not_see_NB Says_unique_NB + Says_Server_imp_YM2 B_trusts_YM4_newK) + + + +(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*) +lemma B_gets_good_key: + "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, + Crypt K (Nonce NB)|} \ set evs; + Says B Server + {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} + \ set evs; + \k. Notes Spy {|Nonce NA, Nonce NB, k|} \ set evs; + A \ bad; B \ bad; evs \ yahalom |] + ==> Key K \ analz (knows Spy evs)" +by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key) + + +(*** Authenticating B to A ***) + +(*The encryption in message YM2 tells us it cannot be faked.*) +lemma B_Said_YM2 [rule_format]: + "[|Crypt (shrK B) {|Agent A, Nonce NA, nb|} \ parts (knows Spy evs); + evs \ yahalom|] + ==> B \ bad --> + Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} + \ set evs" +apply (erule rev_mp, erule yahalom.induct, force, + frule_tac [6] YM4_parts_knows_Spy, simp_all) +(*Fake*) +apply blast +done + +(*If the server sends YM3 then B sent YM2*) +lemma YM3_auth_B_to_A_lemma: + "[|Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} + \ set evs; evs \ yahalom|] + ==> B \ bad --> + Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} + \ set evs" +apply (erule rev_mp, erule yahalom.induct, simp_all) +(*YM3, YM4*) +apply (blast dest!: B_Said_YM2)+ +done + +(*If A receives YM3 then B has used nonce NA (and therefore is alive)*) +lemma YM3_auth_B_to_A: + "[| Gets A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} + \ set evs; + A \ bad; B \ bad; evs \ yahalom |] + ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} + \ set evs" +by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma elim: knows_Spy_partsEs) + + +(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***) + +(*Assuming the session key is secure, if both certificates are present then + A has said NB. We can't be sure about the rest of A's message, but only + NB matters for freshness.*) +lemma A_Said_YM3_lemma [rule_format]: + "evs \ yahalom + ==> Key K \ analz (knows Spy evs) --> + Crypt K (Nonce NB) \ parts (knows Spy evs) --> + Crypt (shrK B) {|Agent A, Key K|} \ parts (knows Spy evs) --> + B \ bad --> + (\X. Says A B {|X, Crypt K (Nonce NB)|} \ set evs)" +apply (erule yahalom.induct, force, + frule_tac [6] YM4_parts_knows_Spy) +apply (analz_mono_contra, simp_all) +(*Fake*) +apply blast +(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*) +apply (force dest!: Crypt_imp_keysFor) +(*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*) +apply (simp add: ex_disj_distrib) +(*yes: apply unicity of session keys*) +apply (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK + Crypt_Spy_analz_bad + dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys) +done + +(*If B receives YM4 then A has used nonce NB (and therefore is alive). + Moreover, A associates K with NB (thus is talking about the same run). + Other premises guarantee secrecy of K.*) +lemma YM4_imp_A_Said_YM3 [rule_format]: + "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, + Crypt K (Nonce NB)|} \ set evs; + Says B Server + {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} + \ set evs; + (\NA k. Notes Spy {|Nonce NA, Nonce NB, k|} \ set evs); + A \ bad; B \ bad; evs \ yahalom |] + ==> \X. Says A B {|X, Crypt K (Nonce NB)|} \ set evs" +by (blast intro!: A_Said_YM3_lemma + dest: Spy_not_see_encrypted_key B_trusts_YM4 Gets_imp_Says) end diff -r c8bbf4c4bc2d -r a6816d47f41d src/HOL/Auth/Yahalom2.ML --- a/src/HOL/Auth/Yahalom2.ML Wed Apr 11 11:53:54 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,378 +0,0 @@ -(* Title: HOL/Auth/Yahalom2 - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1996 University of Cambridge - -Inductive relation "yahalom" for the Yahalom protocol, Variant 2. - -This version trades encryption of NB for additional explicitness in YM3. - -From page 259 of - Burrows, Abadi and Needham. A Logic of Authentication. - Proc. Royal Soc. 426 (1989) -*) - -AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body]; -AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; - - -(*A "possibility property": there are traces that reach the end*) -Goal "\\X NB K. \\evs \\ yahalom. \ -\ Says A B {|X, Crypt K (Nonce NB)|} \\ set evs"; -by (REPEAT (resolve_tac [exI,bexI] 1)); -by (rtac (yahalom.Nil RS - yahalom.YM1 RS yahalom.Reception RS - yahalom.YM2 RS yahalom.Reception RS - yahalom.YM3 RS yahalom.Reception RS yahalom.YM4) 2); -by possibility_tac; -result(); - -Goal "[| Gets B X \\ set evs; evs \\ yahalom |] ==> \\A. Says A B X \\ set evs"; -by (etac rev_mp 1); -by (etac yahalom.induct 1); -by Auto_tac; -qed "Gets_imp_Says"; - -(*Must be proved separately for each protocol*) -Goal "[| Gets B X \\ set evs; evs \\ yahalom |] ==> X \\ knows Spy evs"; -by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1); -qed"Gets_imp_knows_Spy"; -AddDs [Gets_imp_knows_Spy RS parts.Inj]; - - -(**** Inductive proofs about yahalom ****) - -(** For reasoning about the encrypted portion of messages **) - -(*Lets us treat YM4 using a similar argument as for the Fake case.*) -Goal "[| Gets A {|NB, Crypt (shrK A) Y, X|} \\ set evs; evs \\ yahalom |] \ -\ ==> X \\ analz (knows Spy evs)"; -by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1); -qed "YM4_analz_knows_Spy"; - -bind_thm ("YM4_parts_knows_Spy", - YM4_analz_knows_Spy RS (impOfSubs analz_subset_parts)); - -(*For Oops*) -Goal "Says Server A {|NB, Crypt (shrK A) {|B,K,NA|}, X|} \\ set evs \ -\ ==> K \\ parts (knows Spy evs)"; -by (blast_tac (claset() addSDs [parts.Body, - Says_imp_knows_Spy RS parts.Inj]) 1); -qed "YM4_Key_parts_knows_Spy"; - -(*For proving the easier theorems about X \\ parts (knows Spy evs).*) -fun parts_knows_Spy_tac i = - EVERY - [ftac YM4_Key_parts_knows_Spy (i+7), - ftac YM4_parts_knows_Spy (i+6), assume_tac (i+6), - prove_simple_subgoals_tac i]; - -(*Induction for regularity theorems. If induction formula has the form - X \\ analz (knows Spy evs) --> ... then it shortens the proof by discarding - needless information about analz (insert X (knows Spy evs)) *) -fun parts_induct_tac i = - etac yahalom.induct i - THEN - REPEAT (FIRSTGOAL analz_mono_contra_tac) - THEN parts_knows_Spy_tac i; - - -(** Theorems of the form X \\ parts (knows Spy evs) imply that NOBODY - sends messages containing X! **) - -(*Spy never sees another agent's shared key! (unless it's bad at start)*) -Goal "evs \\ yahalom ==> (Key (shrK A) \\ parts (knows Spy evs)) = (A \\ bad)"; -by (parts_induct_tac 1); -by (ALLGOALS Blast_tac); -qed "Spy_see_shrK"; -Addsimps [Spy_see_shrK]; - -Goal "evs \\ yahalom ==> (Key (shrK A) \\ analz (knows Spy evs)) = (A \\ bad)"; -by Auto_tac; -qed "Spy_analz_shrK"; -Addsimps [Spy_analz_shrK]; - -AddSDs [Spy_see_shrK RSN (2, rev_iffD1), - Spy_analz_shrK RSN (2, rev_iffD1)]; - - -(*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*) -Goal "evs \\ yahalom ==> \ -\ Key K \\ used evs --> K \\ keysFor (parts (knows Spy evs))"; -by (parts_induct_tac 1); -(*YM4: Key K is not fresh!*) -by (Blast_tac 3); -(*YM3*) -by (blast_tac (claset() addss (simpset())) 2); -(*Fake*) -by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); -qed_spec_mp "new_keys_not_used"; -Addsimps [new_keys_not_used]; - -(*Earlier, ALL protocol proofs declared this theorem. - But Yahalom and Kerberos IV are the only ones that need it!*) -bind_thm ("new_keys_not_analzd", - [analz_subset_parts RS keysFor_mono, - new_keys_not_used] MRS contra_subsetD); - -(*Describes the form of K when the Server sends this message. Useful for - Oops as well as main secrecy property.*) -Goal "[| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|} \ -\ \\ set evs; \ -\ evs \\ yahalom |] \ -\ ==> K \\ range shrK"; -by (etac rev_mp 1); -by (etac yahalom.induct 1); -by (ALLGOALS Asm_simp_tac); -qed "Says_Server_message_form"; - - -(*For proofs involving analz.*) -val analz_knows_Spy_tac = - dtac YM4_analz_knows_Spy 7 THEN assume_tac 7 THEN - ftac Says_Server_message_form 8 THEN - assume_tac 8 THEN - REPEAT ((etac conjE ORELSE' hyp_subst_tac) 8); - - -(**** - The following is to prove theorems of the form - - Key K \\ analz (insert (Key KAB) (knows Spy evs)) ==> - Key K \\ analz (knows Spy evs) - - A more general formula must be proved inductively. - -****) - -(** Session keys are not used to encrypt other session keys **) - -Goal "evs \\ yahalom ==> \ -\ \\K KK. KK <= - (range shrK) --> \ -\ (Key K \\ analz (Key`KK Un (knows Spy evs))) = \ -\ (K \\ KK | Key K \\ analz (knows Spy evs))"; -by (etac yahalom.induct 1); -by analz_knows_Spy_tac; -by (REPEAT_FIRST (resolve_tac [allI, impI])); -by (REPEAT_FIRST (rtac analz_image_freshK_lemma)); -by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); -(*Fake*) -by (spy_analz_tac 1); -qed_spec_mp "analz_image_freshK"; - -Goal "[| evs \\ yahalom; KAB \\ range shrK |] ==> \ -\ Key K \\ analz (insert (Key KAB) (knows Spy evs)) = \ -\ (K = KAB | Key K \\ analz (knows Spy evs))"; -by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); -qed "analz_insert_freshK"; - - -(*** The Key K uniquely identifies the Server's message. **) - -Goal "[| Says Server A \ -\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} \\ set evs; \ -\ Says Server A' \ -\ {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|} \\ set evs; \ -\ evs \\ yahalom |] \ -\ ==> A=A' & B=B' & na=na' & nb=nb'"; -by (etac rev_mp 1); -by (etac rev_mp 1); -by (etac yahalom.induct 1); -by (ALLGOALS Asm_simp_tac); -(*YM3, by freshness*) -by (Blast_tac 1); -qed "unique_session_keys"; - - -(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **) - -Goal "[| A \\ bad; B \\ bad; evs \\ yahalom |] \ -\ ==> Says Server A \ -\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \ -\ Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \ -\ \\ set evs --> \ -\ Notes Spy {|na, nb, Key K|} \\ set evs --> \ -\ Key K \\ analz (knows Spy evs)"; -by (etac yahalom.induct 1); -by analz_knows_Spy_tac; -by (ALLGOALS - (asm_simp_tac - (simpset() addsimps split_ifs - addsimps [new_keys_not_analzd, analz_insert_eq, - analz_insert_freshK]))); -(*Oops*) -by (blast_tac (claset() addDs [unique_session_keys]) 3); -(*YM3*) -by (Blast_tac 2); -(*Fake*) -by (spy_analz_tac 1); -val lemma = result() RS mp RS mp RSN(2,rev_notE); - - -(*Final version*) -Goal "[| Says Server A \ -\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \ -\ Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \ -\ \\ set evs; \ -\ Notes Spy {|na, nb, Key K|} \\ set evs; \ -\ A \\ bad; B \\ bad; evs \\ yahalom |] \ -\ ==> Key K \\ analz (knows Spy evs)"; -by (blast_tac (claset() addSEs [lemma] addDs [Says_Server_message_form]) 1); -qed "Spy_not_see_encrypted_key"; - - -(** Security Guarantee for A upon receiving YM3 **) - -(*If the encrypted message appears then it originated with the Server. - May now apply Spy_not_see_encrypted_key, subject to its conditions.*) -Goal "[| Crypt (shrK A) {|Agent B, Key K, na|} \ -\ \\ parts (knows Spy evs); \ -\ A \\ bad; evs \\ yahalom |] \ -\ ==> \\nb. Says Server A \ -\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \ -\ Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \ -\ \\ set evs"; -by (etac rev_mp 1); -by (parts_induct_tac 1); -by (ALLGOALS Blast_tac); -qed "A_trusts_YM3"; - -(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*) -Goal "[| Crypt (shrK A) {|Agent B, Key K, na|} \\ parts (knows Spy evs); \ -\ \\nb. Notes Spy {|na, nb, Key K|} \\ set evs; \ -\ A \\ bad; B \\ bad; evs \\ yahalom |] \ -\ ==> Key K \\ analz (knows Spy evs)"; -by (blast_tac (claset() addSDs [A_trusts_YM3, Spy_not_see_encrypted_key]) 1); -qed "A_gets_good_key"; - - -(** Security Guarantee for B upon receiving YM4 **) - -(*B knows, by the first part of A's message, that the Server distributed - the key for A and B, and has associated it with NB.*) -Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|} \ -\ \\ parts (knows Spy evs); \ -\ B \\ bad; evs \\ yahalom |] \ -\ ==> \\NA. Says Server A \ -\ {|Nonce NB, \ -\ Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, \ -\ Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|} \ -\ \\ set evs"; -by (etac rev_mp 1); -by (parts_induct_tac 1); -by (ALLGOALS Blast_tac); -qed "B_trusts_YM4_shrK"; - - -(*With this protocol variant, we don't need the 2nd part of YM4 at all: - Nonce NB is available in the first part.*) - -(*What can B deduce from receipt of YM4? Stronger and simpler than Yahalom - because we do not have to show that NB is secret. *) -Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \ -\ X|} \ -\ \\ set evs; \ -\ A \\ bad; B \\ bad; evs \\ yahalom |] \ -\ ==> \\NA. Says Server A \ -\ {|Nonce NB, \ -\ Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, \ -\ Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|} \ -\ \\ set evs"; -by (blast_tac (claset() addSDs [B_trusts_YM4_shrK]) 1); -qed "B_trusts_YM4"; - - -(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*) -Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \ -\ X|} \ -\ \\ set evs; \ -\ \\na. Notes Spy {|na, Nonce NB, Key K|} \\ set evs; \ -\ A \\ bad; B \\ bad; evs \\ yahalom |] \ -\ ==> Key K \\ analz (knows Spy evs)"; -by (blast_tac (claset() addSDs [B_trusts_YM4, Spy_not_see_encrypted_key]) 1); -qed "B_gets_good_key"; - - - -(*** Authenticating B to A ***) - -(*The encryption in message YM2 tells us it cannot be faked.*) -Goal "[| Crypt (shrK B) {|Agent A, Nonce NA|} \\ parts (knows Spy evs); \ -\ B \\ bad; evs \\ yahalom \ -\ |] ==> \\NB. Says B Server {|Agent B, Nonce NB, \ -\ Crypt (shrK B) {|Agent A, Nonce NA|}|} \ -\ \\ set evs"; -by (etac rev_mp 1); -by (etac rev_mp 1); -by (parts_induct_tac 1); -by (ALLGOALS Blast_tac); -qed "B_Said_YM2"; - - -(*If the server sends YM3 then B sent YM2, perhaps with a different NB*) -Goal "[| Says Server A \ -\ {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \ -\ \\ set evs; \ -\ B \\ bad; evs \\ yahalom \ -\ |] ==> \\nb'. Says B Server {|Agent B, nb', \ -\ Crypt (shrK B) {|Agent A, Nonce NA|}|} \ -\ \\ set evs"; -by (etac rev_mp 1); -by (etac rev_mp 1); -by (etac yahalom.induct 1); -by (ALLGOALS Asm_simp_tac); -(*YM3*) -by (blast_tac (claset() addSDs [B_Said_YM2]) 3); -(*Fake, YM2*) -by (ALLGOALS Blast_tac); -val lemma = result(); - -(*If A receives YM3 then B has used nonce NA (and therefore is alive)*) -Goal "[| Gets A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \ -\ \\ set evs; \ -\ A \\ bad; B \\ bad; evs \\ yahalom |] \ -\==> \\nb'. Says B Server \ -\ {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} \ -\ \\ set evs"; -by (blast_tac (claset() addSDs [A_trusts_YM3, lemma]) 1); -qed "YM3_auth_B_to_A"; - - -(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***) - -(*Assuming the session key is secure, if both certificates are present then - A has said NB. We can't be sure about the rest of A's message, but only - NB matters for freshness. Note that Key K \\ analz (knows Spy evs) must be - the FIRST antecedent of the induction formula.*) -Goal "evs \\ yahalom \ -\ ==> Key K \\ analz (knows Spy evs) --> \ -\ Crypt K (Nonce NB) \\ parts (knows Spy evs) --> \ -\ Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|} \ -\ \\ parts (knows Spy evs) --> \ -\ B \\ bad --> \ -\ (\\X. Says A B {|X, Crypt K (Nonce NB)|} \\ set evs)"; -by (parts_induct_tac 1); -(*Fake*) -by (Blast_tac 1); -(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*) -by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); -(*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*) -by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1); -(*Yes: apply unicity of session keys. [Ind. hyp. no longer needed!]*) -by (blast_tac (claset() addSDs [Gets_imp_Says, A_trusts_YM3, B_trusts_YM4_shrK, - Crypt_Spy_analz_bad] - addDs [Says_imp_spies RS analz.Inj, unique_session_keys]) 1); -qed_spec_mp "Auth_A_to_B_lemma"; - - -(*If B receives YM4 then A has used nonce NB (and therefore is alive). - Moreover, A associates K with NB (thus is talking about the same run). - Other premises guarantee secrecy of K.*) -Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \ -\ Crypt K (Nonce NB)|} \\ set evs; \ -\ (\\NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} \\ set evs); \ -\ A \\ bad; B \\ bad; evs \\ yahalom |] \ -\ ==> \\X. Says A B {|X, Crypt K (Nonce NB)|} \\ set evs"; -by (blast_tac (claset() addIs [Auth_A_to_B_lemma] - addDs [Spy_not_see_encrypted_key, B_trusts_YM4_shrK]) 1); -qed_spec_mp "YM4_imp_A_Said_YM3"; diff -r c8bbf4c4bc2d -r a6816d47f41d src/HOL/Auth/Yahalom2.thy --- a/src/HOL/Auth/Yahalom2.thy Wed Apr 11 11:53:54 2001 +0200 +++ b/src/HOL/Auth/Yahalom2.thy Thu Apr 12 12:45:05 2001 +0200 @@ -13,64 +13,389 @@ Proc. Royal Soc. 426 (1989) *) -Yahalom2 = Shared + +theory Yahalom2 = Shared: -consts yahalom :: event list set +consts yahalom :: "event list set" inductive "yahalom" - intrs + intros (*Initial trace is empty*) - Nil "[] \\ yahalom" + Nil: "[] \ yahalom" (*The spy MAY say anything he CAN say. We do not expect him to invent new nonces here, but he can also use NS1. Common to all similar protocols.*) - Fake "[| evsf \\ yahalom; X \\ synth (analz (knows Spy evsf)) |] - ==> Says Spy B X # evsf \\ yahalom" + Fake: "[| evsf \ yahalom; X \ synth (analz (knows Spy evsf)) |] + ==> Says Spy B X # evsf \ yahalom" (*A message that has been sent can be received by the intended recipient.*) - Reception "[| evsr \\ yahalom; Says A B X \\ set evsr |] - ==> Gets B X # evsr \\ yahalom" + Reception: "[| evsr \ yahalom; Says A B X \ set evsr |] + ==> Gets B X # evsr \ yahalom" (*Alice initiates a protocol run*) - YM1 "[| evs1 \\ yahalom; Nonce NA \\ used evs1 |] - ==> Says A B {|Agent A, Nonce NA|} # evs1 \\ yahalom" + YM1: "[| evs1 \ yahalom; Nonce NA \ used evs1 |] + ==> Says A B {|Agent A, Nonce NA|} # evs1 \ yahalom" (*Bob's response to Alice's message.*) - YM2 "[| evs2 \\ yahalom; Nonce NB \\ used evs2; - Gets B {|Agent A, Nonce NA|} \\ set evs2 |] - ==> Says B Server + YM2: "[| evs2 \ yahalom; Nonce NB \ used evs2; + Gets B {|Agent A, Nonce NA|} \ set evs2 |] + ==> Says B Server {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} - # evs2 \\ yahalom" + # evs2 \ yahalom" (*The Server receives Bob's message. He responds by sending a new session key to Alice, with a certificate for forwarding to Bob. Both agents are quoted in the 2nd certificate to prevent attacks!*) - YM3 "[| evs3 \\ yahalom; Key KAB \\ used evs3; + YM3: "[| evs3 \ yahalom; Key KAB \ used evs3; Gets Server {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} - \\ set evs3 |] + \ set evs3 |] ==> Says Server A - {|Nonce NB, + {|Nonce NB, Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|}, Crypt (shrK B) {|Agent A, Agent B, Key KAB, Nonce NB|}|} - # evs3 \\ yahalom" + # evs3 \ yahalom" (*Alice receives the Server's (?) message, checks her Nonce, and uses the new session key to send Bob his Nonce.*) - YM4 "[| evs4 \\ yahalom; + YM4: "[| evs4 \ yahalom; Gets A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, - X|} \\ set evs4; - Says A B {|Agent A, Nonce NA|} \\ set evs4 |] - ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \\ yahalom" + X|} \ set evs4; + Says A B {|Agent A, Nonce NA|} \ set evs4 |] + ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \ yahalom" (*This message models possible leaks of session keys. The nonces identify the protocol run. Quoting Server here ensures they are correct. *) - Oops "[| evso \\ yahalom; - Says Server A {|Nonce NB, + Oops: "[| evso \ yahalom; + Says Server A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, - X|} \\ set evso |] - ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \\ yahalom" + X|} \ set evso |] + ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \ yahalom" + + +declare Says_imp_knows_Spy [THEN analz.Inj, dest] +declare parts.Body [dest] +declare Fake_parts_insert_in_Un [dest] +declare analz_into_parts [dest] + +(*A "possibility property": there are traces that reach the end*) +lemma "\X NB K. \evs \ yahalom. + Says A B {|X, Crypt K (Nonce NB)|} \ set evs" +apply (intro exI bexI) +apply (rule_tac [2] yahalom.Nil + [THEN yahalom.YM1, THEN yahalom.Reception, + THEN yahalom.YM2, THEN yahalom.Reception, + THEN yahalom.YM3, THEN yahalom.Reception, + THEN yahalom.YM4]) +apply possibility +done + +lemma Gets_imp_Says: + "[| Gets B X \ set evs; evs \ yahalom |] ==> \A. Says A B X \ set evs" +by (erule rev_mp, erule yahalom.induct, auto) + +(*Must be proved separately for each protocol*) +lemma Gets_imp_knows_Spy: + "[| Gets B X \ set evs; evs \ yahalom |] ==> X \ knows Spy evs" +by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) + +declare Gets_imp_knows_Spy [THEN analz.Inj, dest] + + +(**** Inductive proofs about yahalom ****) + +(** For reasoning about the encrypted portion of messages **) + +(*Lets us treat YM4 using a similar argument as for the Fake case.*) +lemma YM4_analz_knows_Spy: + "[| Gets A {|NB, Crypt (shrK A) Y, X|} \ set evs; evs \ yahalom |] + ==> X \ analz (knows Spy evs)" +by blast + +lemmas YM4_parts_knows_Spy = + YM4_analz_knows_Spy [THEN analz_into_parts, standard] + + +(** Theorems of the form X \ parts (knows Spy evs) imply that NOBODY + sends messages containing X! **) + +(*Spy never sees a good agent's shared key!*) +lemma Spy_see_shrK [simp]: + "evs \ yahalom ==> (Key (shrK A) \ parts (knows Spy evs)) = (A \ bad)" +apply (erule yahalom.induct, force, + drule_tac [6] YM4_parts_knows_Spy, simp_all) +apply blast+ +done + +lemma Spy_analz_shrK [simp]: + "evs \ yahalom ==> (Key (shrK A) \ analz (knows Spy evs)) = (A \ bad)" +by auto + +lemma Spy_see_shrK_D [dest!]: + "[|Key (shrK A) \ parts (knows Spy evs); evs \ yahalom|] ==> A \ bad" +by (blast dest: Spy_see_shrK) + +(*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*) +lemma new_keys_not_used [rule_format, simp]: + "evs \ yahalom ==> Key K \ used evs --> K \ keysFor (parts (knows Spy evs))" +apply (erule yahalom.induct, force, + frule_tac [6] YM4_parts_knows_Spy, simp_all) +(*Fake, YM3, YM4*) +apply (blast dest!: keysFor_parts_insert)+ +done + + +(*Describes the form of K when the Server sends this message. Useful for + Oops as well as main secrecy property.*) +lemma Says_Server_message_form: + "[| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|} + \ set evs; evs \ yahalom |] + ==> K \ range shrK" +by (erule rev_mp, erule yahalom.induct, simp_all) + + +(**** + The following is to prove theorems of the form + + Key K \ analz (insert (Key KAB) (knows Spy evs)) ==> + Key K \ analz (knows Spy evs) + + A more general formula must be proved inductively. +****) + +(** Session keys are not used to encrypt other session keys **) + +lemma analz_image_freshK [rule_format]: + "evs \ yahalom ==> + \K KK. KK <= - (range shrK) --> + (Key K \ analz (Key`KK Un (knows Spy evs))) = + (K \ KK | Key K \ analz (knows Spy evs))" +apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form, + drule_tac [6] YM4_analz_knows_Spy) +apply analz_freshK +apply spy_analz +done + +lemma analz_insert_freshK: + "[| evs \ yahalom; KAB \ range shrK |] ==> + Key K \ analz (insert (Key KAB) (knows Spy evs)) = + (K = KAB | Key K \ analz (knows Spy evs))" +by (simp only: analz_image_freshK analz_image_freshK_simps) + + +(*** The Key K uniquely identifies the Server's message. **) + +lemma unique_session_keys: + "[| Says Server A + {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} \ set evs; + Says Server A' + {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|} \ set evs; + evs \ yahalom |] + ==> A=A' & B=B' & na=na' & nb=nb'" +apply (erule rev_mp, erule rev_mp) +apply (erule yahalom.induct, simp_all) +(*YM3, by freshness*) +apply blast +done + + +(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **) + +lemma secrecy_lemma: + "[| A \ bad; B \ bad; evs \ yahalom |] + ==> Says Server A + {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, + Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} + \ set evs --> + Notes Spy {|na, nb, Key K|} \ set evs --> + Key K \ analz (knows Spy evs)" +apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form, + drule_tac [6] YM4_analz_knows_Spy) +apply (simp_all add: pushes analz_insert_eq analz_insert_freshK) +apply spy_analz (*Fake*) +apply (blast dest: unique_session_keys)+ (*YM3, Oops*) +done + + +(*Final version*) +lemma Spy_not_see_encrypted_key: + "[| Says Server A + {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, + Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} + \ set evs; + Notes Spy {|na, nb, Key K|} \ set evs; + A \ bad; B \ bad; evs \ yahalom |] + ==> Key K \ analz (knows Spy evs)" +by (blast dest: secrecy_lemma Says_Server_message_form) + + +(** Security Guarantee for A upon receiving YM3 **) + +(*If the encrypted message appears then it originated with the Server. + May now apply Spy_not_see_encrypted_key, subject to its conditions.*) +lemma A_trusts_YM3: + "[| Crypt (shrK A) {|Agent B, Key K, na|} \ parts (knows Spy evs); + A \ bad; evs \ yahalom |] + ==> \nb. Says Server A + {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, + Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} + \ set evs" +apply (erule rev_mp) +apply (erule yahalom.induct, force, + frule_tac [6] YM4_parts_knows_Spy, simp_all) +(*Fake, YM3*) +apply blast+ +done + +(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*) +lemma A_gets_good_key: + "[| Crypt (shrK A) {|Agent B, Key K, na|} \ parts (knows Spy evs); + \nb. Notes Spy {|na, nb, Key K|} \ set evs; + A \ bad; B \ bad; evs \ yahalom |] + ==> Key K \ analz (knows Spy evs)" +by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key) + + +(** Security Guarantee for B upon receiving YM4 **) + +(*B knows, by the first part of A's message, that the Server distributed + the key for A and B, and has associated it with NB.*) +lemma B_trusts_YM4_shrK: + "[| Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|} + \ parts (knows Spy evs); + B \ bad; evs \ yahalom |] + ==> \NA. Says Server A + {|Nonce NB, + Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, + Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|} + \ set evs" +apply (erule rev_mp) +apply (erule yahalom.induct, force, + frule_tac [6] YM4_parts_knows_Spy, simp_all) +(*Fake, YM3*) +apply blast+ +done + + +(*With this protocol variant, we don't need the 2nd part of YM4 at all: + Nonce NB is available in the first part.*) + +(*What can B deduce from receipt of YM4? Stronger and simpler than Yahalom + because we do not have to show that NB is secret. *) +lemma B_trusts_YM4: + "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, X|} + \ set evs; + A \ bad; B \ bad; evs \ yahalom |] + ==> \NA. Says Server A + {|Nonce NB, + Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, + Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|} + \ set evs" +by (blast dest!: B_trusts_YM4_shrK) + + +(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*) +lemma B_gets_good_key: + "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, X|} + \ set evs; + \na. Notes Spy {|na, Nonce NB, Key K|} \ set evs; + A \ bad; B \ bad; evs \ yahalom |] + ==> Key K \ analz (knows Spy evs)" +by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key) + + +(*** Authenticating B to A ***) + +(*The encryption in message YM2 tells us it cannot be faked.*) +lemma B_Said_YM2: + "[| Crypt (shrK B) {|Agent A, Nonce NA|} \ parts (knows Spy evs); + B \ bad; evs \ yahalom |] + ==> \NB. Says B Server {|Agent B, Nonce NB, + Crypt (shrK B) {|Agent A, Nonce NA|}|} + \ set evs" +apply (erule rev_mp) +apply (erule yahalom.induct, force, + frule_tac [6] YM4_parts_knows_Spy, simp_all) +(*Fake, YM2*) +apply blast+ +done + + +(*If the server sends YM3 then B sent YM2, perhaps with a different NB*) +lemma YM3_auth_B_to_A_lemma: + "[| Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} + \ set evs; + B \ bad; evs \ yahalom |] + ==> \nb'. Says B Server {|Agent B, nb', + Crypt (shrK B) {|Agent A, Nonce NA|}|} + \ set evs" +apply (erule rev_mp) +apply (erule yahalom.induct, simp_all) +(*Fake, YM2, YM3*) +apply (blast dest!: B_Said_YM2)+ +done + +(*If A receives YM3 then B has used nonce NA (and therefore is alive)*) +lemma YM3_auth_B_to_A: + "[| Gets A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} + \ set evs; + A \ bad; B \ bad; evs \ yahalom |] + ==> \nb'. Says B Server + {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} + \ set evs" +by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma) + + + +(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***) + +(*Assuming the session key is secure, if both certificates are present then + A has said NB. We can't be sure about the rest of A's message, but only + NB matters for freshness. Note that Key K \ analz (knows Spy evs) must be + the FIRST antecedent of the induction formula.*) + +(*This lemma allows a use of unique_session_keys in the next proof, + which otherwise is extremely slow.*) +lemma secure_unique_session_keys: + "[| Crypt (shrK A) {|Agent B, Key K, na|} \ analz (spies evs); + Crypt (shrK A') {|Agent B', Key K, na'|} \ analz (spies evs); + Key K \ analz (knows Spy evs); evs \ yahalom |] + ==> A=A' & B=B'" +by (blast dest!: A_trusts_YM3 dest: unique_session_keys Crypt_Spy_analz_bad) + + +lemma Auth_A_to_B_lemma [rule_format]: + "evs \ yahalom + ==> Key K \ analz (knows Spy evs) --> + Crypt K (Nonce NB) \ parts (knows Spy evs) --> + Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|} + \ parts (knows Spy evs) --> + B \ bad --> + (\X. Says A B {|X, Crypt K (Nonce NB)|} \ set evs)" +apply (erule yahalom.induct, force, + frule_tac [6] YM4_parts_knows_Spy) +apply (analz_mono_contra, simp_all) +(*Fake*) +apply blast +(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*) +apply (force dest!: Crypt_imp_keysFor) +(*YM4: was Crypt K (Nonce NB) the very last message? If so, apply unicity + of session keys; if not, use ind. hyp.*) +apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys ) +done + + +(*If B receives YM4 then A has used nonce NB (and therefore is alive). + Moreover, A associates K with NB (thus is talking about the same run). + Other premises guarantee secrecy of K.*) +lemma YM4_imp_A_Said_YM3 [rule_format]: + "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, + Crypt K (Nonce NB)|} \ set evs; + (\NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} \ set evs); + A \ bad; B \ bad; evs \ yahalom |] + ==> \X. Says A B {|X, Crypt K (Nonce NB)|} \ set evs" +by (blast intro: Auth_A_to_B_lemma + dest: Spy_not_see_encrypted_key B_trusts_YM4_shrK) end diff -r c8bbf4c4bc2d -r a6816d47f41d src/HOL/Auth/Yahalom_Bad.ML --- a/src/HOL/Auth/Yahalom_Bad.ML Wed Apr 11 11:53:54 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,329 +0,0 @@ -(* Title: HOL/Auth/Yahalom - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1996 University of Cambridge - -Inductive relation "yahalom" for the Yahalom protocol. - -From page 257 of - Burrows, Abadi and Needham. A Logic of Authentication. - Proc. Royal Soc. 426 (1989) -*) - -(*A "possibility property": there are traces that reach the end*) -Goal "A \\ Server \ -\ ==> \\X NB K. \\evs \\ yahalom. \ -\ Says A B {|X, Crypt K (Nonce NB)|} \\ set evs"; -by (REPEAT (resolve_tac [exI,bexI] 1)); -by (rtac (yahalom.Nil RS - yahalom.YM1 RS yahalom.Reception RS - yahalom.YM2 RS yahalom.Reception RS - yahalom.YM3 RS yahalom.Reception RS yahalom.YM4) 2); -by possibility_tac; -result(); - -Goal "[| Gets B X \\ set evs; evs \\ yahalom |] ==> \\A. Says A B X \\ set evs"; -by (etac rev_mp 1); -by (etac yahalom.induct 1); -by Auto_tac; -qed "Gets_imp_Says"; - -(*Must be proved separately for each protocol*) -Goal "[| Gets B X \\ set evs; evs \\ yahalom |] ==> X \\ knows Spy evs"; -by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1); -qed"Gets_imp_knows_Spy"; -AddDs [Gets_imp_knows_Spy RS parts.Inj]; - - -(**** Inductive proofs about yahalom ****) - - -(** For reasoning about the encrypted portion of messages **) - -(*Lets us treat YM4 using a similar argument as for the Fake case.*) -Goal "[| Gets A {|Crypt (shrK A) Y, X|} \\ set evs; evs \\ yahalom |] \ -\ ==> X \\ analz (knows Spy evs)"; -by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1); -qed "YM4_analz_knows_Spy"; - -bind_thm ("YM4_parts_knows_Spy", - YM4_analz_knows_Spy RS (impOfSubs analz_subset_parts)); - -(*For proving the easier theorems about X \\ parts (knows Spy evs).*) -fun parts_knows_Spy_tac i = - EVERY - [ftac YM4_parts_knows_Spy (i+6), assume_tac (i+6), - prove_simple_subgoals_tac i]; - -(*Induction for regularity theorems. If induction formula has the form - X \\ analz (knows Spy evs) --> ... then it shortens the proof by discarding - needless information about analz (insert X (knows Spy evs)) *) -fun parts_induct_tac i = - etac yahalom.induct i - THEN - REPEAT (FIRSTGOAL analz_mono_contra_tac) - THEN parts_knows_Spy_tac i; - - -(** Theorems of the form X \\ parts (knows Spy evs) imply that NOBODY - sends messages containing X! **) - -(*Spy never sees another agent's shared key! (unless it's bad at start)*) -Goal "evs \\ yahalom ==> (Key (shrK A) \\ parts (knows Spy evs)) = (A \\ bad)"; -by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); -by (ALLGOALS Blast_tac); -qed "Spy_see_shrK"; -Addsimps [Spy_see_shrK]; - -Goal "evs \\ yahalom ==> (Key (shrK A) \\ analz (knows Spy evs)) = (A \\ bad)"; -by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); -qed "Spy_analz_shrK"; -Addsimps [Spy_analz_shrK]; - -AddSDs [Spy_see_shrK RSN (2, rev_iffD1), - Spy_analz_shrK RSN (2, rev_iffD1)]; - - -(*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*) -Goal "evs \\ yahalom ==> \ -\ Key K \\ used evs --> K \\ keysFor (parts (knows Spy evs))"; -by (parts_induct_tac 1); -(*Fake*) -by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); -(*YM2-4: Because Key K is not fresh, etc.*) -by (REPEAT (blast_tac (claset() addSEs knows_Spy_partsEs) 1)); -qed_spec_mp "new_keys_not_used"; -Addsimps [new_keys_not_used]; - - -(*For proofs involving analz.*) -val analz_knows_Spy_tac = - ftac YM4_analz_knows_Spy 7 THEN assume_tac 7; - -(**** - The following is to prove theorems of the form - - Key K \\ analz (insert (Key KAB) (knows Spy evs)) ==> - Key K \\ analz (knows Spy evs) - - A more general formula must be proved inductively. -****) - -(** Session keys are not used to encrypt other session keys **) - -Goal "evs \\ yahalom ==> \ -\ \\K KK. KK <= - (range shrK) --> \ -\ (Key K \\ analz (Key`KK Un (knows Spy evs))) = \ -\ (K \\ KK | Key K \\ analz (knows Spy evs))"; -by (etac yahalom.induct 1); -by analz_knows_Spy_tac; -by (REPEAT_FIRST (resolve_tac [allI, impI])); -by (REPEAT_FIRST (rtac analz_image_freshK_lemma)); -by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); -(*Fake*) -by (spy_analz_tac 1); -qed_spec_mp "analz_image_freshK"; - -Goal "[| evs \\ yahalom; KAB \\ range shrK |] \ -\ ==> Key K \\ analz (insert (Key KAB) (knows Spy evs)) = \ -\ (K = KAB | Key K \\ analz (knows Spy evs))"; -by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); -qed "analz_insert_freshK"; - - -(*** The Key K uniquely identifies the Server's message. **) - -Goal "[| Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \\ set evs; \ -\ Says Server A' \ -\ {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} \\ set evs; \ -\ evs \\ yahalom |] \ -\ ==> A=A' & B=B' & na=na' & nb=nb'"; -by (etac rev_mp 1); -by (etac rev_mp 1); -by (etac yahalom.induct 1); -by (ALLGOALS Asm_simp_tac); -(*YM4*) -by (Blast_tac 2); -(*YM3, by freshness*) -by (blast_tac (claset() addSEs knows_Spy_partsEs) 1); -qed "unique_session_keys"; - - -(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **) - -Goal "[| A \\ bad; B \\ bad; evs \\ yahalom |] \ -\ ==> Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \ -\ Crypt (shrK B) {|Agent A, Key K|}|} \ -\ \\ set evs --> \ -\ Key K \\ analz (knows Spy evs)"; -by (etac yahalom.induct 1); -by analz_knows_Spy_tac; -by (ALLGOALS - (asm_simp_tac - (simpset() addsimps split_ifs @ pushes @ - [analz_insert_eq, analz_insert_freshK]))); -(*YM3*) -by (blast_tac (claset() delrules [impCE] - addSEs knows_Spy_partsEs - addIs [impOfSubs analz_subset_parts]) 2); -(*Fake*) -by (spy_analz_tac 1); -val lemma = result() RS mp RSN(2,rev_notE); - - -(*Final version*) -Goal "[| Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \ -\ Crypt (shrK B) {|Agent A, Key K|}|} \ -\ \\ set evs; \ -\ A \\ bad; B \\ bad; evs \\ yahalom |] \ -\ ==> Key K \\ analz (knows Spy evs)"; -by (blast_tac (claset() addSEs [lemma]) 1); -qed "Spy_not_see_encrypted_key"; - - -(** Security Guarantee for A upon receiving YM3 **) - -(*If the encrypted message appears then it originated with the Server*) -Goal "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \\ parts (knows Spy evs); \ -\ A \\ bad; evs \\ yahalom |] \ -\ ==> Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \ -\ Crypt (shrK B) {|Agent A, Key K|}|} \ -\ \\ set evs"; -by (etac rev_mp 1); -by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); -qed "A_trusts_YM3"; - -(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*) -Goal "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \\ parts (knows Spy evs); \ -\ A \\ bad; B \\ bad; evs \\ yahalom |] \ -\ ==> Key K \\ analz (knows Spy evs)"; -by (blast_tac (claset() addSDs [A_trusts_YM3, Spy_not_see_encrypted_key]) 1); -qed "A_gets_good_key"; - -(** Security Guarantees for B upon receiving YM4 **) - -(*B knows, by the first part of A's message, that the Server distributed - the key for A and B. But this part says nothing about nonces.*) -Goal "[| Crypt (shrK B) {|Agent A, Key K|} \\ parts (knows Spy evs); \ -\ B \\ bad; evs \\ yahalom |] \ -\ ==> \\NA NB. Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, \ -\ Nonce NA, Nonce NB|}, \ -\ Crypt (shrK B) {|Agent A, Key K|}|} \ -\ \\ set evs"; -by (etac rev_mp 1); -by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); -(*YM3*) -by (Blast_tac 1); -qed "B_trusts_YM4_shrK"; - -(** Up to now, the reasoning is similar to standard Yahalom. Now the - doubtful reasoning occurs. We should not be assuming that an unknown - key is secure, but the model allows us to: there is no Oops rule to - let session keys go.*) - -(*B knows, by the second part of A's message, that the Server distributed - the key quoting nonce NB. This part says nothing about agent names. - Secrecy of K is assumed; the valid Yahalom proof uses (and later proves) - the secrecy of NB.*) -Goal "evs \\ yahalom \ -\ ==> Key K \\ analz (knows Spy evs) --> \ -\ Crypt K (Nonce NB) \\ parts (knows Spy evs) --> \ -\ (\\A B NA. Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, \ -\ Nonce NA, Nonce NB|}, \ -\ Crypt (shrK B) {|Agent A, Key K|}|} \ -\ \\ set evs)"; -by (parts_induct_tac 1); -by (ALLGOALS Clarify_tac); -(*YM3 & Fake*) -by (Blast_tac 2); -by (Fake_parts_insert_tac 1); -(*YM4*) -(*A is uncompromised because NB is secure; - A's certificate guarantees the existence of the Server message*) -by (blast_tac (claset() addSDs [Gets_imp_Says, Crypt_Spy_analz_bad] - addDs [Says_imp_spies, analz.Inj, - parts.Inj RS parts.Fst RS A_trusts_YM3]) 1); -bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp)); - - -(*B's session key guarantee from YM4. The two certificates contribute to a - single conclusion about the Server's message. *) -Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, \ -\ Crypt K (Nonce NB)|} \\ set evs; \ -\ Says B Server \ -\ {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} \ -\ \\ set evs; \ -\ A \\ bad; B \\ bad; evs \\ yahalom |] \ -\ ==> \\na nb. Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \ -\ Crypt (shrK B) {|Agent A, Key K|}|} \ -\ \\ set evs"; -by (blast_tac (claset() addDs [B_trusts_YM4_newK, B_trusts_YM4_shrK, - Spy_not_see_encrypted_key, unique_session_keys]) 1); -qed "B_trusts_YM4"; - - -(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*) -Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, \ -\ Crypt K (Nonce NB)|} \\ set evs; \ -\ Says B Server \ -\ {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} \ -\ \\ set evs; \ -\ A \\ bad; B \\ bad; evs \\ yahalom |] \ -\ ==> Key K \\ analz (knows Spy evs)"; -by (blast_tac (claset() addSDs [B_trusts_YM4, Spy_not_see_encrypted_key]) 1); -qed "B_gets_good_key"; - - -(*** Authenticating B to A: these proofs are not considered. - They are irrelevant to showing the need for Oops. ***) - - -(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***) - -(*Assuming the session key is secure, if both certificates are present then - A has said NB. We can't be sure about the rest of A's message, but only - NB matters for freshness.*) -Goal "evs \\ yahalom \ -\ ==> Key K \\ analz (knows Spy evs) --> \ -\ Crypt K (Nonce NB) \\ parts (knows Spy evs) --> \ -\ Crypt (shrK B) {|Agent A, Key K|} \\ parts (knows Spy evs) --> \ -\ B \\ bad --> \ -\ (\\X. Says A B {|X, Crypt K (Nonce NB)|} \\ set evs)"; -by (parts_induct_tac 1); -(*Fake*) -by (Fake_parts_insert_tac 1); -(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*) -by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); -(*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*) -by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1); -(*yes: apply unicity of session keys*) -by (blast_tac (claset() addSDs [Gets_imp_Says, A_trusts_YM3, B_trusts_YM4_shrK, - Crypt_Spy_analz_bad] - addDs [Says_imp_knows_Spy RS parts.Inj, - Says_imp_spies RS analz.Inj, unique_session_keys]) 1); -qed_spec_mp "A_Said_YM3_lemma"; - -(*If B receives YM4 then A has used nonce NB (and therefore is alive). - Moreover, A associates K with NB (thus is talking about the same run). - Other premises guarantee secrecy of K.*) -Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, \ -\ Crypt K (Nonce NB)|} \\ set evs; \ -\ Says B Server \ -\ {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} \ -\ \\ set evs; \ -\ A \\ bad; B \\ bad; evs \\ yahalom |] \ -\ ==> \\X. Says A B {|X, Crypt K (Nonce NB)|} \\ set evs"; -by (blast_tac (claset() addSIs [A_Said_YM3_lemma] - addDs [Spy_not_see_encrypted_key, B_trusts_YM4, - Gets_imp_Says, Says_imp_knows_Spy RS parts.Inj]) 1); -qed_spec_mp "YM4_imp_A_Said_YM3"; diff -r c8bbf4c4bc2d -r a6816d47f41d src/HOL/Auth/Yahalom_Bad.thy --- a/src/HOL/Auth/Yahalom_Bad.thy Wed Apr 11 11:53:54 2001 +0200 +++ b/src/HOL/Auth/Yahalom_Bad.thy Thu Apr 12 12:45:05 2001 +0200 @@ -5,62 +5,354 @@ Inductive relation "yahalom" for the Yahalom protocol. -Example of why Oops is necessary. This protocol can be attacked because it -doesn't keep NB secret, but without Oops it can be "verified" anyway. +Demonstrates of why Oops is necessary. This protocol can be attacked because +it doesn't keep NB secret, but without Oops it can be "verified" anyway. +The issues are discussed in lcp's LICS 2000 invited lecture. *) -Yahalom_Bad = Shared + +theory Yahalom_Bad = Shared: -consts yahalom :: event list set +consts yahalom :: "event list set" inductive "yahalom" - intrs + intros (*Initial trace is empty*) - Nil "[] : yahalom" + Nil: "[] \ yahalom" (*The spy MAY say anything he CAN say. We do not expect him to invent new nonces here, but he can also use NS1. Common to all similar protocols.*) - Fake "[| evsf \\ yahalom; X \\ synth (analz (knows Spy evsf)) |] - ==> Says Spy B X # evsf \\ yahalom" + Fake: "[| evsf \ yahalom; X \ synth (analz (knows Spy evsf)) |] + ==> Says Spy B X # evsf \ yahalom" (*A message that has been sent can be received by the intended recipient.*) - Reception "[| evsr \\ yahalom; Says A B X \\ set evsr |] - ==> Gets B X # evsr \\ yahalom" + Reception: "[| evsr \ yahalom; Says A B X \ set evsr |] + ==> Gets B X # evsr \ yahalom" (*Alice initiates a protocol run*) - YM1 "[| evs1 \\ yahalom; Nonce NA \\ used evs1 |] - ==> Says A B {|Agent A, Nonce NA|} # evs1 \\ yahalom" + YM1: "[| evs1 \ yahalom; Nonce NA \ used evs1 |] + ==> Says A B {|Agent A, Nonce NA|} # evs1 \ yahalom" (*Bob's response to Alice's message.*) - YM2 "[| evs2 \\ yahalom; Nonce NB \\ used evs2; - Gets B {|Agent A, Nonce NA|} \\ set evs2 |] - ==> Says B Server + YM2: "[| evs2 \ yahalom; Nonce NB \ used evs2; + Gets B {|Agent A, Nonce NA|} \ set evs2 |] + ==> Says B Server {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} - # evs2 \\ yahalom" + # evs2 \ yahalom" (*The Server receives Bob's message. He responds by sending a new session key to Alice, with a packet for forwarding to Bob.*) - YM3 "[| evs3 \\ yahalom; Key KAB \\ used evs3; - Gets Server + YM3: "[| evs3 \ yahalom; Key KAB \ used evs3; + Gets Server {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} - \\ set evs3 |] + \ set evs3 |] ==> Says Server A {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|}, Crypt (shrK B) {|Agent A, Key KAB|}|} - # evs3 \\ yahalom" + # evs3 \ yahalom" (*Alice receives the Server's (?) message, checks her Nonce, and uses the new session key to send Bob his Nonce. The premise - A \\ Server is needed to prove Says_Server_not_range.*) - YM4 "[| evs4 \\ yahalom; A \\ Server; + A \ Server is needed to prove Says_Server_not_range.*) + YM4: "[| evs4 \ yahalom; A \ Server; Gets A {|Crypt(shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|} - \\ set evs4; - Says A B {|Agent A, Nonce NA|} \\ set evs4 |] - ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \\ yahalom" + \ set evs4; + Says A B {|Agent A, Nonce NA|} \ set evs4 |] + ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \ yahalom" + + +declare Says_imp_knows_Spy [THEN analz.Inj, dest] +declare parts.Body [dest] +declare Fake_parts_insert_in_Un [dest] +declare analz_into_parts [dest] + + +(*A "possibility property": there are traces that reach the end*) +lemma "A \ Server + ==> \X NB K. \evs \ yahalom. + Says A B {|X, Crypt K (Nonce NB)|} \ set evs" +apply (intro exI bexI) +apply (rule_tac [2] yahalom.Nil + [THEN yahalom.YM1, THEN yahalom.Reception, + THEN yahalom.YM2, THEN yahalom.Reception, + THEN yahalom.YM3, THEN yahalom.Reception, + THEN yahalom.YM4]) +apply possibility +done + +lemma Gets_imp_Says: + "[| Gets B X \ set evs; evs \ yahalom |] ==> \A. Says A B X \ set evs" +by (erule rev_mp, erule yahalom.induct, auto) + +(*Must be proved separately for each protocol*) +lemma Gets_imp_knows_Spy: + "[| Gets B X \ set evs; evs \ yahalom |] ==> X \ knows Spy evs" +by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) + +declare Gets_imp_knows_Spy [THEN analz.Inj, dest] + + +(**** Inductive proofs about yahalom ****) + +(** For reasoning about the encrypted portion of messages **) + +(*Lets us treat YM4 using a similar argument as for the Fake case.*) +lemma YM4_analz_knows_Spy: + "[| Gets A {|Crypt (shrK A) Y, X|} \ set evs; evs \ yahalom |] + ==> X \ analz (knows Spy evs)" +by blast + +lemmas YM4_parts_knows_Spy = + YM4_analz_knows_Spy [THEN analz_into_parts, standard] + + +(** Theorems of the form X \ parts (knows Spy evs) imply that NOBODY + sends messages containing X! **) + +(*Spy never sees a good agent's shared key!*) +lemma Spy_see_shrK [simp]: + "evs \ yahalom ==> (Key (shrK A) \ parts (knows Spy evs)) = (A \ bad)" +apply (erule yahalom.induct, force, + drule_tac [6] YM4_parts_knows_Spy, simp_all) +apply blast+ +done + +lemma Spy_analz_shrK [simp]: + "evs \ yahalom ==> (Key (shrK A) \ analz (knows Spy evs)) = (A \ bad)" +by auto + +lemma Spy_see_shrK_D [dest!]: + "[|Key (shrK A) \ parts (knows Spy evs); evs \ yahalom|] ==> A \ bad" +by (blast dest: Spy_see_shrK) + +(*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*) +lemma new_keys_not_used [rule_format, simp]: + "evs \ yahalom ==> Key K \ used evs --> K \ keysFor (parts (knows Spy evs))" +apply (erule yahalom.induct, force, + frule_tac [6] YM4_parts_knows_Spy, simp_all) +(*Fake, YM3, YM4*) +apply (blast dest!: keysFor_parts_insert)+ +done + + +(**** + The following is to prove theorems of the form + + Key K \ analz (insert (Key KAB) (knows Spy evs)) ==> + Key K \ analz (knows Spy evs) + + A more general formula must be proved inductively. +****) + +(** Session keys are not used to encrypt other session keys **) + +lemma analz_image_freshK [rule_format]: + "evs \ yahalom ==> + \K KK. KK <= - (range shrK) --> + (Key K \ analz (Key`KK Un (knows Spy evs))) = + (K \ KK | Key K \ analz (knows Spy evs))" +apply (erule yahalom.induct, force, + drule_tac [6] YM4_analz_knows_Spy) +apply analz_freshK +apply spy_analz +done + +lemma analz_insert_freshK: "[| evs \ yahalom; KAB \ range shrK |] ==> + Key K \ analz (insert (Key KAB) (knows Spy evs)) = + (K = KAB | Key K \ analz (knows Spy evs))" +by (simp only: analz_image_freshK analz_image_freshK_simps) + + +(*** The Key K uniquely identifies the Server's message. **) + +lemma unique_session_keys: + "[| Says Server A + {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \ set evs; + Says Server A' + {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} \ set evs; + evs \ yahalom |] + ==> A=A' & B=B' & na=na' & nb=nb'" +apply (erule rev_mp, erule rev_mp) +apply (erule yahalom.induct, simp_all) +(*YM3, by freshness, and YM4*) +apply blast+ +done + + +(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **) + +lemma secrecy_lemma: + "[| A \ bad; B \ bad; evs \ yahalom |] + ==> Says Server A + {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, + Crypt (shrK B) {|Agent A, Key K|}|} + \ set evs --> + Key K \ analz (knows Spy evs)" +apply (erule yahalom.induct, force, drule_tac [6] YM4_analz_knows_Spy) +apply (simp_all add: pushes analz_insert_eq analz_insert_freshK) +apply spy_analz (*Fake*) +apply (blast dest: unique_session_keys) (*YM3*) +done + +(*Final version*) +lemma Spy_not_see_encrypted_key: + "[| Says Server A + {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, + Crypt (shrK B) {|Agent A, Key K|}|} + \ set evs; + A \ bad; B \ bad; evs \ yahalom |] + ==> Key K \ analz (knows Spy evs)" +by (blast dest: secrecy_lemma) + - (*This message models possible leaks of session keys. The Nonces - identify the protocol run. Quoting Server here ensures they are - correct.*) +(** Security Guarantee for A upon receiving YM3 **) + +(*If the encrypted message appears then it originated with the Server*) +lemma A_trusts_YM3: + "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \ parts (knows Spy evs); + A \ bad; evs \ yahalom |] + ==> Says Server A + {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, + Crypt (shrK B) {|Agent A, Key K|}|} + \ set evs" +apply (erule rev_mp) +apply (erule yahalom.induct, force, + frule_tac [6] YM4_parts_knows_Spy, simp_all) +(*Fake, YM3*) +apply blast+ +done + +(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*) +lemma A_gets_good_key: + "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \ parts (knows Spy evs); + A \ bad; B \ bad; evs \ yahalom |] + ==> Key K \ analz (knows Spy evs)" +by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key) + +(** Security Guarantees for B upon receiving YM4 **) + +(*B knows, by the first part of A's message, that the Server distributed + the key for A and B. But this part says nothing about nonces.*) +lemma B_trusts_YM4_shrK: + "[| Crypt (shrK B) {|Agent A, Key K|} \ parts (knows Spy evs); + B \ bad; evs \ yahalom |] + ==> \NA NB. Says Server A + {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, + Crypt (shrK B) {|Agent A, Key K|}|} + \ set evs" +apply (erule rev_mp) +apply (erule yahalom.induct, force, + frule_tac [6] YM4_parts_knows_Spy, simp_all) +(*Fake, YM3*) +apply blast+ +done + +(** Up to now, the reasoning is similar to standard Yahalom. Now the + doubtful reasoning occurs. We should not be assuming that an unknown + key is secure, but the model allows us to: there is no Oops rule to + let session keys become compromised.*) + +(*B knows, by the second part of A's message, that the Server distributed + the key quoting nonce NB. This part says nothing about agent names. + Secrecy of K is assumed; the valid Yahalom proof uses (and later proves) + the secrecy of NB.*) +lemma B_trusts_YM4_newK [rule_format]: + "[|Key K \ analz (knows Spy evs); evs \ yahalom|] + ==> Crypt K (Nonce NB) \ parts (knows Spy evs) --> + (\A B NA. Says Server A + {|Crypt (shrK A) {|Agent B, Key K, + Nonce NA, Nonce NB|}, + Crypt (shrK B) {|Agent A, Key K|}|} + \ set evs)" +apply (erule rev_mp) +apply (erule yahalom.induct, force, + frule_tac [6] YM4_parts_knows_Spy) +apply (analz_mono_contra, simp_all) +(*Fake*) +apply blast +(*YM3*) +apply blast +(*A is uncompromised because NB is secure + A's certificate guarantees the existence of the Server message*) +apply (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad + dest: Says_imp_spies + parts.Inj [THEN parts.Fst, THEN A_trusts_YM3]) +done + + +(*B's session key guarantee from YM4. The two certificates contribute to a + single conclusion about the Server's message. *) +lemma B_trusts_YM4: + "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, + Crypt K (Nonce NB)|} \ set evs; + Says B Server + {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} + \ set evs; + A \ bad; B \ bad; evs \ yahalom |] + ==> \na nb. Says Server A + {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, + Crypt (shrK B) {|Agent A, Key K|}|} + \ set evs" +by (blast dest: B_trusts_YM4_newK B_trusts_YM4_shrK Spy_not_see_encrypted_key + unique_session_keys) + + +(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*) +lemma B_gets_good_key: + "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, + Crypt K (Nonce NB)|} \ set evs; + Says B Server + {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} + \ set evs; + A \ bad; B \ bad; evs \ yahalom |] + ==> Key K \ analz (knows Spy evs)" +by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key) + + +(*** Authenticating B to A: these proofs are not considered. + They are irrelevant to showing the need for Oops. ***) + + +(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***) + +(*Assuming the session key is secure, if both certificates are present then + A has said NB. We can't be sure about the rest of A's message, but only + NB matters for freshness.*) +lemma A_Said_YM3_lemma [rule_format]: + "evs \ yahalom + ==> Key K \ analz (knows Spy evs) --> + Crypt K (Nonce NB) \ parts (knows Spy evs) --> + Crypt (shrK B) {|Agent A, Key K|} \ parts (knows Spy evs) --> + B \ bad --> + (\X. Says A B {|X, Crypt K (Nonce NB)|} \ set evs)" +apply (erule yahalom.induct, force, + frule_tac [6] YM4_parts_knows_Spy) +apply (analz_mono_contra, simp_all) +(*Fake*) +apply blast +(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*) +apply (force dest!: Crypt_imp_keysFor) +(*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*) +apply (simp add: ex_disj_distrib) +(*yes: apply unicity of session keys*) +apply (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK + Crypt_Spy_analz_bad + dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys) +done + +(*If B receives YM4 then A has used nonce NB (and therefore is alive). + Moreover, A associates K with NB (thus is talking about the same run). + Other premises guarantee secrecy of K.*) +lemma YM4_imp_A_Said_YM3 [rule_format]: + "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, + Crypt K (Nonce NB)|} \ set evs; + Says B Server + {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} + \ set evs; + A \ bad; B \ bad; evs \ yahalom |] + ==> \X. Says A B {|X, Crypt K (Nonce NB)|} \ set evs" +apply (blast intro!: A_Said_YM3_lemma + dest: Spy_not_see_encrypted_key B_trusts_YM4 Gets_imp_Says) +done end diff -r c8bbf4c4bc2d -r a6816d47f41d src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Apr 11 11:53:54 2001 +0200 +++ b/src/HOL/IsaMakefile Thu Apr 12 12:45:05 2001 +0200 @@ -304,15 +304,13 @@ $(LOG)/HOL-Auth.gz: $(OUT)/HOL Auth/Event_lemmas.ML Auth/Event.thy \ Auth/Message_lemmas.ML Auth/Message.thy Auth/NS_Public.thy \ Auth/NS_Public_Bad.thy \ - Auth/NS_Shared.thy Auth/OtwayRees.ML Auth/OtwayRees.thy \ - Auth/OtwayRees_AN.ML Auth/OtwayRees_AN.thy Auth/OtwayRees_Bad.ML \ + Auth/NS_Shared.thy Auth/OtwayRees.thy Auth/OtwayRees_AN.thy \ Auth/OtwayRees_Bad.thy Auth/Public_lemmas.ML Auth/Public.thy Auth/ROOT.ML \ Auth/Recur.ML Auth/Recur.thy Auth/Shared_lemmas.ML Auth/Shared.thy \ - Auth/TLS.ML Auth/TLS.thy Auth/WooLam.ML Auth/WooLam.thy \ + Auth/TLS.ML Auth/TLS.thy Auth/WooLam.thy \ Auth/Kerberos_BAN.ML Auth/Kerberos_BAN.thy \ Auth/KerberosIV.ML Auth/KerberosIV.thy \ - Auth/Yahalom.ML Auth/Yahalom.thy Auth/Yahalom2.ML Auth/Yahalom2.thy \ - Auth/Yahalom_Bad.ML Auth/Yahalom_Bad.thy + Auth/Yahalom.thy Auth/Yahalom2.thy Auth/Yahalom_Bad.thy @$(ISATOOL) usedir $(OUT)/HOL Auth