diff -r 2a3cc8e1723a -r f2024fed9f0c src/HOL/Auth/KerberosIV.ML --- a/src/HOL/Auth/KerberosIV.ML Tue Feb 13 01:32:54 2001 +0100 +++ b/src/HOL/Auth/KerberosIV.ML Tue Feb 13 13:16:27 2001 +0100 @@ -358,7 +358,7 @@ \ Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}) \ \ | ServTicket : analz (spies evs)"; by (case_tac "Key AuthKey : analz (spies evs)" 1); -by (force_tac (claset() addSDs [Says_imp_spies RS analz.Inj], simpset()) 1); +by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]) 1); by (forward_tac [Says_imp_spies RS parts.Inj] 1); by (blast_tac (claset() addSDs [ServTicket_form]) 1); qed "Says_tgs_message_form"; @@ -370,54 +370,38 @@ (* The session key, if secure, uniquely identifies the Ticket whether AuthTicket or ServTicket. As a matter of fact, one can read also Tgs in the place of B. *) -Goal "evs : kerberos ==> \ -\ Key SesKey ~: analz (spies evs) --> \ -\ (EX A B T. ALL A' B' T'. \ -\ Crypt (shrK B') {|Agent A', Agent B', Key SesKey, T'|} \ -\ : parts (spies evs) --> A'=A & B'=B & T'=T)"; -by (parts_induct_tac 1); -by (REPEAT (etac (exI RSN (2,exE)) 1) (*stripping EXs makes proof faster*) - THEN Fake_parts_insert_tac 1); -by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1); -by (expand_case_tac "SesKey = ?y" 1); -by (blast_tac (claset() addSEs spies_partsEs) 1); -by (expand_case_tac "SesKey = ?y" 1); -by (blast_tac (claset() addSEs spies_partsEs) 1); -val lemma = result(); Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key SesKey, T|} \ \ : parts (spies evs); \ \ Crypt (shrK B') {|Agent A', Agent B', Key SesKey, T'|} \ -\ : parts (spies evs); \ -\ evs : kerberos; Key SesKey ~: analz (spies evs) |] \ +\ : parts (spies evs); Key SesKey ~: analz (spies evs); \ +\ evs : kerberos |] \ \ ==> A=A' & B=B' & T=T'"; -by (prove_unique_tac lemma 1); +by (etac rev_mp 1); +by (etac rev_mp 1); +by (etac rev_mp 1); +by (parts_induct_tac 1); +(*Fake, K2, K4*) +by (Fake_parts_insert_tac 1); +by (REPEAT (blast_tac (claset() addSEs knows_Spy_partsEs) 1)); qed "unique_CryptKey"; -Goal "evs : kerberos \ -\ ==> Key SesKey ~: analz (spies evs) --> \ -\ (EX K' B' T' Ticket'. ALL K B T Ticket. \ -\ Crypt K {|Key SesKey, Agent B, T, Ticket|} \ -\ : parts (spies evs) --> K=K' & B=B' & T=T' & Ticket=Ticket')"; -by (parts_induct_tac 1); -by (REPEAT (etac (exI RSN (2,exE)) 1) THEN Fake_parts_insert_tac 1); -by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1); -by (expand_case_tac "SesKey = ?y" 1); -by (blast_tac (claset() addSEs spies_partsEs) 1); -by (expand_case_tac "SesKey = ?y" 1); -by (blast_tac (claset() addSEs spies_partsEs) 1); -val lemma = result(); - (*An AuthKey is encrypted by one and only one Shared key. A ServKey is encrypted by one and only one AuthKey. *) Goal "[| Crypt K {|Key SesKey, Agent B, T, Ticket|} \ \ : parts (spies evs); \ \ Crypt K' {|Key SesKey, Agent B', T', Ticket'|} \ -\ : parts (spies evs); \ -\ evs : kerberos; Key SesKey ~: analz (spies evs) |] \ +\ : parts (spies evs); Key SesKey ~: analz (spies evs); \ +\ evs : kerberos |] \ \ ==> K=K' & B=B' & T=T' & Ticket=Ticket'"; -by (prove_unique_tac lemma 1); +by (etac rev_mp 1); +by (etac rev_mp 1); +by (etac rev_mp 1); +by (parts_induct_tac 1); +(*Fake, K2, K4*) +by (Fake_parts_insert_tac 1); +by (REPEAT (blast_tac (claset() addSEs knows_Spy_partsEs) 1)); qed "Key_unique_SesKey"; @@ -439,50 +423,29 @@ would fail on the K2 and K4 cases. *) -(* AuthKey uniquely identifies the message from Kas *) -Goal "evs : kerberos ==> \ -\ EX A' Ka' Tk' X'. ALL A Ka Tk X. \ -\ Says Kas A (Crypt Ka {|Key AuthKey, Agent Tgs, Tk, X|}) \ -\ : set evs --> A=A' & Ka=Ka' & Tk=Tk' & X=X'"; -by (etac kerberos.induct 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); -by (Step_tac 1); -(*K2: it can't be a new key*) -by (expand_case_tac "AuthKey = ?y" 1); -by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); -by (blast_tac (claset() delrules [conjI] (*prevent split-up into 4 subgoals*) - addSEs spies_partsEs) 1); -val lemma = result(); - Goal "[| Says Kas A \ \ (Crypt Ka {|Key AuthKey, Agent Tgs, Tk, X|}) : set evs; \ \ Says Kas A' \ \ (Crypt Ka' {|Key AuthKey, Agent Tgs, Tk', X'|}) : set evs; \ \ evs : kerberos |] ==> A=A' & Ka=Ka' & Tk=Tk' & X=X'"; -by (prove_unique_tac lemma 1); +by (etac rev_mp 1); +by (etac rev_mp 1); +by (parts_induct_tac 1); +(*K2*) +by (blast_tac (claset() addSEs knows_Spy_partsEs) 1); qed "unique_AuthKeys"; (* ServKey uniquely identifies the message from Tgs *) -Goal "evs : kerberos ==> \ -\ EX A' B' AuthKey' Tk' X'. ALL A B AuthKey Tk X. \ -\ Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tk, X|}) \ -\ : set evs --> A=A' & B=B' & AuthKey=AuthKey' & Tk=Tk' & X=X'"; -by (etac kerberos.induct 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); -by (Step_tac 1); -(*K4: it can't be a new key*) -by (expand_case_tac "ServKey = ?y" 1); -by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); -by (blast_tac (claset() delrules [conjI] (*prevent split-up into 4 subgoals*) - addSEs spies_partsEs) 1); -val lemma = result(); - Goal "[| Says Tgs A \ \ (Crypt K {|Key ServKey, Agent B, Tt, X|}) : set evs; \ \ Says Tgs A' \ \ (Crypt K' {|Key ServKey, Agent B', Tt', X'|}) : set evs; \ \ evs : kerberos |] ==> A=A' & B=B' & K=K' & Tt=Tt' & X=X'"; -by (prove_unique_tac lemma 1); +by (etac rev_mp 1); +by (etac rev_mp 1); +by (parts_induct_tac 1); +(*K4*) +by (blast_tac (claset() addSEs knows_Spy_partsEs) 1); qed "unique_ServKeys";