diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/Yahalom2.ML --- a/src/HOL/Auth/Yahalom2.ML Mon Jul 14 12:44:09 1997 +0200 +++ b/src/HOL/Auth/Yahalom2.ML Mon Jul 14 12:47:21 1997 +0200 @@ -18,13 +18,13 @@ HOL_quantifiers := false; (*Replacing the variable by a constant improves speed*) -val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy; +val Says_imp_sees_Spy' = Says_imp_sees_Spy; (*A "possibility property": there are traces that reach the end*) goal thy - "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ -\ ==> EX X NB K. EX evs: yahalom lost. \ + "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ +\ ==> 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 @@ -36,7 +36,7 @@ (**** Inductive proofs about yahalom ****) (*Nobody sends themselves messages*) -goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set evs"; +goal thy "!!evs. evs: yahalom ==> ALL A X. Says A A X ~: set evs"; by (etac yahalom.induct 1); by (Auto_tac()); qed_spec_mp "not_Says_to_self"; @@ -48,7 +48,7 @@ (*Lets us treat YM4 using a similar argument as for the Fake case.*) goal thy "!!evs. Says S A {|NB, Crypt (shrK A) Y, X|} : set evs ==> \ -\ X : analz (sees lost Spy evs)"; +\ X : analz (sees Spy evs)"; by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1); qed "YM4_analz_sees_Spy"; @@ -57,45 +57,47 @@ (*Relates to both YM4 and Oops*) goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B,K,NA|}, X|} : set evs ==> \ -\ K : parts (sees lost Spy evs)"; +\ K : parts (sees Spy evs)"; by (blast_tac (!claset addSEs partsEs addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1); qed "YM4_Key_parts_sees_Spy"; -(*For proving the easier theorems about X ~: parts (sees lost Spy evs). - We instantiate the variable to "lost" since leaving it as a Var would - interfere with simplification.*) -val parts_sees_tac = - forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6 THEN - forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7 THEN - prove_simple_subgoals_tac 1; +(*For proving the easier theorems about X ~: parts (sees Spy evs).*) +fun parts_sees_tac i = + forward_tac [YM4_Key_parts_sees_Spy] (i+6) THEN + forward_tac [YM4_parts_sees_Spy] (i+5) THEN + prove_simple_subgoals_tac i; -val parts_induct_tac = - etac yahalom.induct 1 THEN parts_sees_tac; +(*Induction for regularity theorems. If induction formula has the form + X ~: analz (sees Spy evs) --> ... then it shortens the proof by discarding + needless information about analz (insert X (sees Spy evs)) *) +fun parts_induct_tac i = + etac yahalom.induct i + THEN + REPEAT (FIRSTGOAL analz_mono_contra_tac) + THEN parts_sees_tac i; -(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY +(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY sends messages containing X! **) (*Spy never sees another agent's shared key! (unless it's lost at start)*) goal thy - "!!evs. evs : yahalom lost \ -\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; -by parts_induct_tac; + "!!evs. evs : yahalom ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)"; +by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); by (Blast_tac 1); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; goal thy - "!!evs. evs : yahalom lost \ -\ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)"; + "!!evs. evs : yahalom ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)"; by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); qed "Spy_analz_shrK"; Addsimps [Spy_analz_shrK]; -goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \ -\ evs : yahalom lost |] ==> A:lost"; +goal thy "!!A. [| Key (shrK A) : parts (sees Spy evs); \ +\ evs : yahalom |] ==> A:lost"; by (blast_tac (!claset addDs [Spy_see_shrK]) 1); qed "Spy_see_shrK_D"; @@ -104,9 +106,9 @@ (*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*) -goal thy "!!evs. evs : yahalom lost ==> \ -\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))"; -by parts_induct_tac; +goal thy "!!evs. evs : yahalom ==> \ +\ Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))"; +by (parts_induct_tac 1); (*YM4: Key K is not fresh!*) by (blast_tac (!claset addSEs sees_Spy_partsEs) 3); (*YM3*) @@ -129,8 +131,8 @@ Oops as well as main secrecy property.*) goal thy "!!evs. [| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|} \ -\ : set evs; \ -\ evs : yahalom lost |] \ +\ : set evs; \ +\ evs : yahalom |] \ \ ==> K ~: range shrK & A ~= B"; by (etac rev_mp 1); by (etac yahalom.induct 1); @@ -138,10 +140,10 @@ qed "Says_Server_message_form"; -(*For proofs involving analz. We again instantiate the variable to "lost".*) +(*For proofs involving analz.*) val analz_sees_tac = - dres_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN - forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN + dtac YM4_analz_sees_Spy 6 THEN + forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN REPEAT ((etac conjE ORELSE' hyp_subst_tac) 7); @@ -149,8 +151,8 @@ (**** The following is to prove theorems of the form - Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==> - Key K : analz (sees lost Spy evs) + Key K : analz (insert (Key KAB) (sees Spy evs)) ==> + Key K : analz (sees Spy evs) A more general formula must be proved inductively. @@ -159,10 +161,10 @@ (** Session keys are not used to encrypt other session keys **) goal thy - "!!evs. evs : yahalom lost ==> \ -\ ALL K KK. KK <= Compl (range shrK) --> \ -\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \ -\ (K : KK | Key K : analz (sees lost Spy evs))"; + "!!evs. evs : yahalom ==> \ +\ ALL K KK. KK <= Compl (range shrK) --> \ +\ (Key K : analz (Key``KK Un (sees Spy evs))) = \ +\ (K : KK | Key K : analz (sees Spy evs))"; by (etac yahalom.induct 1); by analz_sees_tac; by (REPEAT_FIRST (resolve_tac [allI, impI])); @@ -175,9 +177,9 @@ qed_spec_mp "analz_image_freshK"; goal thy - "!!evs. [| evs : yahalom lost; KAB ~: range shrK |] ==> \ -\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \ -\ (K = KAB | Key K : analz (sees lost Spy evs))"; + "!!evs. [| evs : yahalom; KAB ~: range shrK |] ==> \ +\ Key K : analz (insert (Key KAB) (sees Spy evs)) = \ +\ (K = KAB | Key K : analz (sees Spy evs))"; by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); qed "analz_insert_freshK"; @@ -185,10 +187,10 @@ (*** The Key K uniquely identifies the Server's message. **) goal thy - "!!evs. evs : yahalom lost ==> \ -\ EX A' B' na' nb' X'. ALL A B na nb X. \ -\ Says Server A \ -\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} \ + "!!evs. evs : yahalom ==> \ +\ EX A' B' na' nb' X'. ALL A B na nb X. \ +\ Says Server A \ +\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} \ \ : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'"; by (etac yahalom.induct 1); by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); @@ -198,8 +200,8 @@ by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); (*...we assume X is a recent message and handle this case by contradiction*) by (blast_tac (!claset addSEs sees_Spy_partsEs - delrules [conjI] (*prevent split-up into 4 subgoals*) - addss (!simpset addsimps [parts_insertI])) 1); + delrules [conjI] (*prevent split-up into 4 subgoals*) + addss (!simpset addsimps [parts_insertI])) 1); val lemma = result(); goal thy @@ -209,7 +211,7 @@ \ Says Server A' \ \ {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|} \ \ : set evs; \ -\ evs : yahalom lost |] \ +\ evs : yahalom |] \ \ ==> A=A' & B=B' & na=na' & nb=nb'"; by (prove_unique_tac lemma 1); qed "unique_session_keys"; @@ -218,14 +220,14 @@ (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **) goal thy - "!!evs. [| A ~: lost; B ~: lost; A ~= B; \ -\ evs : yahalom lost |] \ -\ ==> Says Server A \ -\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \ -\ Crypt (shrK B) {|nb, Key K, Agent A|}|} \ -\ : set evs --> \ -\ Says A Spy {|na, nb, Key K|} ~: set evs --> \ -\ Key K ~: analz (sees lost Spy evs)"; + "!!evs. [| A ~: lost; B ~: lost; A ~= B; \ +\ evs : yahalom |] \ +\ ==> Says Server A \ +\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \ +\ Crypt (shrK B) {|nb, Key K, Agent A|}|} \ +\ : set evs --> \ +\ Says A Spy {|na, nb, Key K|} ~: set evs --> \ +\ Key K ~: analz (sees Spy evs)"; by (etac yahalom.induct 1); by analz_sees_tac; by (ALLGOALS @@ -246,13 +248,13 @@ (*Final version*) goal thy - "!!evs. [| Says Server A \ -\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \ -\ Crypt (shrK B) {|nb, Key K, Agent A|}|} \ -\ : set evs; \ -\ Says A Spy {|na, nb, Key K|} ~: set evs; \ -\ A ~: lost; B ~: lost; evs : yahalom lost |] \ -\ ==> Key K ~: analz (sees lost Spy evs)"; + "!!evs. [| Says Server A \ +\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \ +\ Crypt (shrK B) {|nb, Key K, Agent A|}|} \ +\ : set evs; \ +\ Says A Spy {|na, nb, Key K|} ~: set evs; \ +\ A ~: lost; B ~: lost; evs : yahalom |] \ +\ ==> Key K ~: analz (sees 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"; @@ -264,14 +266,14 @@ May now apply Spy_not_see_encrypted_key, subject to its conditions.*) goal thy "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na|} \ -\ : parts (sees lost Spy evs); \ -\ A ~: lost; evs : yahalom lost |] \ +\ : parts (sees Spy evs); \ +\ A ~: lost; evs : yahalom |] \ \ ==> EX nb. Says Server A \ \ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \ \ Crypt (shrK B) {|nb, Key K, Agent A|}|} \ \ : set evs"; by (etac rev_mp 1); -by parts_induct_tac; +by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); by (Blast_tac 1); qed "A_trusts_YM3"; @@ -283,15 +285,15 @@ the key for A and B, and has associated it with NB. *) goal thy "!!evs. [| Crypt (shrK B) {|Nonce NB, Key K, Agent A|} \ -\ : parts (sees lost Spy evs); \ -\ B ~: lost; evs : yahalom lost |] \ +\ : parts (sees Spy evs); \ +\ B ~: lost; evs : yahalom |] \ \ ==> EX NA. Says Server A \ \ {|Nonce NB, \ \ Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, \ \ Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|} \ \ : set evs"; by (etac rev_mp 1); -by parts_induct_tac; +by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); (*YM3*) by (Blast_tac 1); @@ -306,7 +308,7 @@ goal thy "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|}, X|} \ \ : set evs; \ -\ A ~: lost; B ~: lost; evs : yahalom lost |] \ +\ A ~: lost; B ~: lost; evs : yahalom |] \ \ ==> EX NA. Says Server A \ \ {|Nonce NB, \ \ Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, \ @@ -322,13 +324,13 @@ (*The encryption in message YM2 tells us it cannot be faked.*) goal thy - "!!evs. evs : yahalom lost \ -\ ==> Crypt (shrK B) {|Agent A, Nonce NA|} : parts (sees lost Spy evs) --> \ -\ B ~: lost --> \ -\ (EX NB. Says B Server {|Agent B, Nonce NB, \ -\ Crypt (shrK B) {|Agent A, Nonce NA|}|} \ + "!!evs. evs : yahalom \ +\ ==> Crypt (shrK B) {|Agent A, Nonce NA|} : parts (sees Spy evs) --> \ +\ B ~: lost --> \ +\ (EX NB. Says B Server {|Agent B, Nonce NB, \ +\ Crypt (shrK B) {|Agent A, Nonce NA|}|} \ \ : set evs)"; -by parts_induct_tac; +by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); (*YM2*) by (Blast_tac 1); @@ -336,7 +338,7 @@ (*If the server sends YM3 then B sent YM2, perhaps with a different NB*) goal thy - "!!evs. evs : yahalom lost \ + "!!evs. evs : yahalom \ \ ==> Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \ \ : set evs --> \ \ B ~: lost --> \ @@ -357,7 +359,7 @@ goal thy "!!evs. [| Says S A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \ \ : set evs; \ -\ A ~: lost; B ~: lost; evs : yahalom lost |] \ +\ A ~: lost; B ~: lost; evs : yahalom |] \ \ ==> EX nb'. Says B Server \ \ {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} \ \ : set evs"; @@ -368,29 +370,18 @@ (*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***) -(*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ... - It simplifies the proof by discarding needless information about - analz (insert X (sees lost Spy evs)) -*) -fun analz_mono_parts_induct_tac i = - etac yahalom.induct i - THEN - REPEAT_FIRST analz_mono_contra_tac - THEN parts_sees_tac; - - (*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 thy - "!!evs. evs : yahalom lost \ -\ ==> Key K ~: analz (sees lost Spy evs) --> \ -\ Crypt K (Nonce NB) : parts (sees lost Spy evs) --> \ -\ Crypt (shrK B) {|Nonce NB, Key K, Agent A|} \ -\ : parts (sees lost Spy evs) --> \ -\ B ~: lost --> \ + "!!evs. evs : yahalom \ +\ ==> Key K ~: analz (sees Spy evs) --> \ +\ Crypt K (Nonce NB) : parts (sees Spy evs) --> \ +\ Crypt (shrK B) {|Nonce NB, Key K, Agent A|} \ +\ : parts (sees Spy evs) --> \ +\ B ~: lost --> \ \ (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)"; -by (analz_mono_parts_induct_tac 1); +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*) @@ -412,7 +403,7 @@ "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|}, \ \ Crypt K (Nonce NB)|} : set evs; \ \ (ALL NA. Says A Spy {|Nonce NA, Nonce NB, Key K|} ~: set evs); \ -\ A ~: lost; B ~: lost; evs : yahalom lost |] \ +\ A ~: lost; B ~: lost; evs : yahalom |] \ \ ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs"; by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1); by (dtac B_trusts_YM4_shrK 1);