diff -r e53457213857 -r 7e4bffaa2a3e src/HOL/Auth/Yahalom2.ML --- a/src/HOL/Auth/Yahalom2.ML Wed Mar 10 10:42:40 1999 +0100 +++ b/src/HOL/Auth/Yahalom2.ML Wed Mar 10 10:42:57 1999 +0100 @@ -12,7 +12,7 @@ Proc. Royal Soc. 426 (1989) *) -AddEs spies_partsEs; +AddEs knows_Spy_partsEs; AddDs [impOfSubs analz_subset_parts]; AddDs [impOfSubs Fake_parts_insert]; @@ -21,58 +21,74 @@ Goal "EX X NB K. EX 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.YM2 RS yahalom.YM3 RS - yahalom.YM4) 2); +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 |] ==> EX 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 "Says S A {|NB, Crypt (shrK A) Y, X|} : set evs ==> \ -\ X : analz (spies evs)"; -by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1); -qed "YM4_analz_spies"; +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_spies", - YM4_analz_spies RS (impOfSubs analz_subset_parts)); +bind_thm ("YM4_parts_knows_Spy", + YM4_analz_knows_Spy RS (impOfSubs analz_subset_parts)); -(*Relates to both YM4 and Oops*) -Goal "Says S A {|NB, Crypt (shrK A) {|B,K,NA|}, X|} : set evs ==> \ -\ K : parts (spies evs)"; -by (Blast_tac 1); -qed "YM4_Key_parts_spies"; +(*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() addSEs partsEs + addSDs [Says_imp_knows_Spy RS parts.Inj]) 1); +qed "YM4_Key_parts_knows_Spy"; -(*For proving the easier theorems about X ~: parts (spies evs).*) -fun parts_spies_tac i = - forward_tac [YM4_Key_parts_spies] (i+6) THEN - forward_tac [YM4_parts_spies] (i+5) THEN - prove_simple_subgoals_tac i; +(*For proving the easier theorems about X ~: parts (knows Spy evs).*) +fun parts_knows_Spy_tac i = + EVERY + [forward_tac [YM4_Key_parts_knows_Spy] (i+7), + forward_tac [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 (spies evs) --> ... then it shortens the proof by discarding - needless information about analz (insert X (spies evs)) *) + 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_spies_tac i; + THEN parts_knows_Spy_tac i; -(** Theorems of the form X ~: parts (spies evs) imply that NOBODY +(** 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 (spies evs)) = (A : bad)"; +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 (spies evs)) = (A : bad)"; +Goal "evs : yahalom ==> (Key (shrK A) : analz (knows Spy evs)) = (A : bad)"; by Auto_tac; qed "Spy_analz_shrK"; Addsimps [Spy_analz_shrK]; @@ -83,7 +99,7 @@ (*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*) Goal "evs : yahalom ==> \ -\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; +\ 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); @@ -112,18 +128,18 @@ (*For proofs involving analz.*) -val analz_spies_tac = - dtac YM4_analz_spies 6 THEN - forward_tac [Says_Server_message_form] 7 THEN - assume_tac 7 THEN - REPEAT ((etac conjE ORELSE' hyp_subst_tac) 7); +val analz_knows_Spy_tac = + dtac YM4_analz_knows_Spy 7 THEN assume_tac 7 THEN + forward_tac [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) (spies evs)) ==> - Key K : analz (spies evs) + Key K : analz (insert (Key KAB) (knows Spy evs)) ==> + Key K : analz (knows Spy evs) A more general formula must be proved inductively. @@ -133,10 +149,10 @@ Goal "evs : yahalom ==> \ \ ALL K KK. KK <= - (range shrK) --> \ -\ (Key K : analz (Key``KK Un (spies evs))) = \ -\ (K : KK | Key K : analz (spies evs))"; +\ (Key K : analz (Key``KK Un (knows Spy evs))) = \ +\ (K : KK | Key K : analz (knows Spy evs))"; by (etac yahalom.induct 1); -by analz_spies_tac; +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)); @@ -145,8 +161,8 @@ qed_spec_mp "analz_image_freshK"; Goal "[| evs : yahalom; KAB ~: range shrK |] ==> \ -\ Key K : analz (insert (Key KAB) (spies evs)) = \ -\ (K = KAB | Key K : analz (spies evs))"; +\ 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"; @@ -187,9 +203,9 @@ \ Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \ \ : set evs --> \ \ Notes Spy {|na, nb, Key K|} ~: set evs --> \ -\ Key K ~: analz (spies evs)"; +\ Key K ~: analz (knows Spy evs)"; by (etac yahalom.induct 1); -by analz_spies_tac; +by analz_knows_Spy_tac; by (ALLGOALS (asm_simp_tac (simpset() addsimps split_ifs @@ -211,7 +227,7 @@ \ : set evs; \ \ Notes Spy {|na, nb, Key K|} ~: set evs; \ \ A ~: bad; B ~: bad; evs : yahalom |] \ -\ ==> Key K ~: analz (spies evs)"; +\ ==> Key K ~: analz (knows Spy evs)"; by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); by (blast_tac (claset() addSEs [lemma]) 1); qed "Spy_not_see_encrypted_key"; @@ -222,7 +238,7 @@ (*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 (spies evs); \ +\ : parts (knows Spy evs); \ \ A ~: bad; evs : yahalom |] \ \ ==> EX nb. Says Server A \ \ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \ @@ -234,10 +250,10 @@ 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 (spies evs); \ +Goal "[| Crypt (shrK A) {|Agent B, Key K, na|} : parts (knows Spy evs); \ \ ALL nb. Notes Spy {|na, nb, Key K|} ~: set evs; \ \ A ~: bad; B ~: bad; evs : yahalom |] \ -\ ==> Key K ~: analz (spies evs)"; +\ ==> 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"; @@ -247,7 +263,7 @@ (*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 (spies evs); \ +\ : parts (knows Spy evs); \ \ B ~: bad; evs : yahalom |] \ \ ==> EX NA. Says Server A \ \ {|Nonce NB, \ @@ -265,7 +281,7 @@ (*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 "[| Says A' B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \ +Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \ \ X|} \ \ : set evs; \ \ A ~: bad; B ~: bad; evs : yahalom |] \ @@ -279,12 +295,12 @@ (*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*) -Goal "[| Says A' B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \ +Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \ \ X|} \ \ : set evs; \ \ ALL na. Notes Spy {|na, Nonce NB, Key K|} ~: set evs; \ \ A ~: bad; B ~: bad; evs : yahalom |] \ -\ ==> Key K ~: analz (spies evs)"; +\ ==> 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"; @@ -293,7 +309,7 @@ (*** Authenticating B to A ***) (*The encryption in message YM2 tells us it cannot be faked.*) -Goal "[| Crypt (shrK B) {|Agent A, Nonce NA|} : parts (spies evs); \ +Goal "[| Crypt (shrK B) {|Agent A, Nonce NA|} : parts (knows Spy evs); \ \ B ~: bad; evs : yahalom \ \ |] ==> EX NB. Says B Server {|Agent B, Nonce NB, \ \ Crypt (shrK B) {|Agent A, Nonce NA|}|} \ @@ -324,9 +340,9 @@ val lemma = result(); (*If A receives YM3 then B has used nonce NA (and therefore is alive)*) -Goal "[| Says S A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \ +Goal "[| Gets A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \ \ : set evs; \ -\ A ~: bad; B ~: bad; evs : yahalom |] \ +\ A ~: bad; B ~: bad; evs : yahalom |] \ \==> EX nb'. Says B Server \ \ {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} \ \ : set evs"; @@ -338,13 +354,13 @@ (*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 (spies evs) must be + 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 (spies evs) --> \ -\ Crypt K (Nonce NB) : parts (spies evs) --> \ +\ ==> 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 (spies evs) --> \ +\ : parts (knows Spy evs) --> \ \ B ~: bad --> \ \ (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)"; by (parts_induct_tac 1); @@ -356,6 +372,7 @@ by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1); (*yes: delete a useless induction hypothesis; apply unicity of session keys*) by (thin_tac "?P-->?Q" 1); +by (forward_tac [Gets_imp_Says] 1 THEN assume_tac 1); by (not_bad_tac "Aa" 1); by (blast_tac (claset() addSDs [A_trusts_YM3, B_trusts_YM4_shrK] addDs [unique_session_keys]) 1); @@ -365,12 +382,12 @@ (*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 "[| Says A' B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \ +Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \ \ Crypt K (Nonce NB)|} : set evs; \ \ (ALL NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} ~: set evs); \ \ A ~: bad; B ~: bad; evs : yahalom |] \ \ ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs"; -by (subgoal_tac "Key K ~: analz (spies evs)" 1); +by (subgoal_tac "Key K ~: analz (knows Spy evs)" 1); by (blast_tac (claset() addIs [Auth_A_to_B_lemma]) 1); by (blast_tac (claset() addDs [Spy_not_see_encrypted_key, B_trusts_YM4_shrK]) 1);