# HG changeset patch # User paulson # Date 903708874 -7200 # Node ID bd539b72d4849f5e673fbcecc20407dfdc97b2fd # Parent 7e046ef59fe22550f82bf573a0776c0fc4ec3ebf Tidying diff -r 7e046ef59fe2 -r bd539b72d484 src/HOL/Auth/Kerberos_BAN.ML --- a/src/HOL/Auth/Kerberos_BAN.ML Fri Aug 21 15:56:12 1998 +0200 +++ b/src/HOL/Auth/Kerberos_BAN.ML Fri Aug 21 16:14:34 1998 +0200 @@ -16,9 +16,6 @@ Tidied by lcp. *) -proof_timing:=true; -HOL_quantifiers := false; - AddEs spies_partsEs; AddDs [impOfSubs analz_subset_parts]; AddDs [impOfSubs Fake_parts_insert]; diff -r 7e046ef59fe2 -r bd539b72d484 src/HOL/Auth/NS_Public.ML --- a/src/HOL/Auth/NS_Public.ML Fri Aug 21 15:56:12 1998 +0200 +++ b/src/HOL/Auth/NS_Public.ML Fri Aug 21 16:14:34 1998 +0200 @@ -7,9 +7,6 @@ Version incorporating Lowe's fix (inclusion of B's identify in round 2). *) -set proof_timing; -HOL_quantifiers := false; - AddEs spies_partsEs; AddDs [impOfSubs analz_subset_parts]; AddDs [impOfSubs Fake_parts_insert]; diff -r 7e046ef59fe2 -r bd539b72d484 src/HOL/Auth/NS_Public_Bad.ML --- a/src/HOL/Auth/NS_Public_Bad.ML Fri Aug 21 15:56:12 1998 +0200 +++ b/src/HOL/Auth/NS_Public_Bad.ML Fri Aug 21 16:14:34 1998 +0200 @@ -11,8 +11,6 @@ Proc. Royal Soc. 426 (1989) *) -HOL_quantifiers := false; - AddEs spies_partsEs; AddDs [impOfSubs analz_subset_parts]; AddDs [impOfSubs Fake_parts_insert]; diff -r 7e046ef59fe2 -r bd539b72d484 src/HOL/Auth/NS_Shared.ML --- a/src/HOL/Auth/NS_Shared.ML Fri Aug 21 15:56:12 1998 +0200 +++ b/src/HOL/Auth/NS_Shared.ML Fri Aug 21 16:14:34 1998 +0200 @@ -10,8 +10,6 @@ Proc. Royal Soc. 426 (1989) *) -HOL_quantifiers := false; - AddEs spies_partsEs; AddDs [impOfSubs analz_subset_parts]; AddDs [impOfSubs Fake_parts_insert]; diff -r 7e046ef59fe2 -r bd539b72d484 src/HOL/Auth/NS_Shared.thy --- a/src/HOL/Auth/NS_Shared.thy Fri Aug 21 15:56:12 1998 +0200 +++ b/src/HOL/Auth/NS_Shared.thy Fri Aug 21 16:14:34 1998 +0200 @@ -71,8 +71,7 @@ (*This message models possible leaks of session keys. The two Nonces identify the protocol run: the rule insists upon the true senders in order to make them accurate.*) - Oops "[| evso: ns_shared; A ~= Spy; - Says B A (Crypt K (Nonce NB)) : set evso; + Oops "[| evso: ns_shared; Says B A (Crypt K (Nonce NB)) : set evso; Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) : set evso |] ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : ns_shared" diff -r 7e046ef59fe2 -r bd539b72d484 src/HOL/Auth/OtwayRees.ML --- a/src/HOL/Auth/OtwayRees.ML Fri Aug 21 15:56:12 1998 +0200 +++ b/src/HOL/Auth/OtwayRees.ML Fri Aug 21 16:14:34 1998 +0200 @@ -92,8 +92,7 @@ (*Nobody can have used non-existent keys!*) -Goal "evs : otway ==> \ -\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; +Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; by (parts_induct_tac 1); (*Fake*) by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); @@ -114,7 +113,7 @@ (*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 |] \ +\ evs : otway |] \ \ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; by (etac rev_mp 1); by (etac otway.induct 1); @@ -144,23 +143,22 @@ (** 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 <= Compl (range shrK) --> \ -\ (Key K : analz (Key``KK Un (spies evs))) = \ -\ (K : KK | Key K : analz (spies evs))"; +Goal "evs : otway ==> ALL K KK. KK <= Compl (range shrK) --> \ +\ (Key K : analz (Key``KK Un (spies evs))) = \ +\ (K : KK | Key K : analz (spies evs))"; by (etac otway.induct 1); by analz_spies_tac; by (REPEAT_FIRST (resolve_tac [allI, impI])); -by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); +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) (spies evs)) = \ -\ (K = KAB | Key K : analz (spies evs))"; +Goal "[| evs : otway; KAB ~: range shrK |] \ +\ ==> Key K : analz (insert (Key KAB) (spies evs)) = \ +\ (K = KAB | Key K : analz (spies evs))"; by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); qed "analz_insert_freshK"; @@ -168,8 +166,8 @@ (*** The Key K uniquely identifies the Server's message. **) Goal "evs : otway ==> \ -\ EX B' NA' NB' X'. ALL B NA NB X. \ -\ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \ +\ EX B' NA' NB' X'. ALL B NA NB X. \ +\ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \ \ B=B' & NA=NA' & NB=NB' & X=X'"; by (etac otway.induct 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); diff -r 7e046ef59fe2 -r bd539b72d484 src/HOL/Auth/OtwayRees.thy --- a/src/HOL/Auth/OtwayRees.thy Fri Aug 21 15:56:12 1998 +0200 +++ b/src/HOL/Auth/OtwayRees.thy Fri Aug 21 16:14:34 1998 +0200 @@ -72,7 +72,7 @@ (*This message models possible leaks of session keys. The nonces identify the protocol run.*) - Oops "[| evso: otway; B ~= Spy; + 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" diff -r 7e046ef59fe2 -r bd539b72d484 src/HOL/Auth/OtwayRees_AN.thy --- a/src/HOL/Auth/OtwayRees_AN.thy Fri Aug 21 15:56:12 1998 +0200 +++ b/src/HOL/Auth/OtwayRees_AN.thy Fri Aug 21 16:14:34 1998 +0200 @@ -63,7 +63,7 @@ (*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; B ~= Spy; + 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|}|} diff -r 7e046ef59fe2 -r bd539b72d484 src/HOL/Auth/OtwayRees_Bad.thy --- a/src/HOL/Auth/OtwayRees_Bad.thy Fri Aug 21 15:56:12 1998 +0200 +++ b/src/HOL/Auth/OtwayRees_Bad.thy Fri Aug 21 16:14:34 1998 +0200 @@ -69,7 +69,7 @@ (*This message models possible leaks of session keys. The nonces identify the protocol run.*) - Oops "[| evso: otway; B ~= Spy; + 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" diff -r 7e046ef59fe2 -r bd539b72d484 src/HOL/Auth/ROOT.ML --- a/src/HOL/Auth/ROOT.ML Fri Aug 21 15:56:12 1998 +0200 +++ b/src/HOL/Auth/ROOT.ML Fri Aug 21 16:14:34 1998 +0200 @@ -11,6 +11,7 @@ writeln"Root file for HOL/Auth"; set proof_timing; goals_limit := 1; +HOL_quantifiers := false; (*Shared-key protocols*) time_use_thy "NS_Shared"; diff -r 7e046ef59fe2 -r bd539b72d484 src/HOL/Auth/Recur.ML --- a/src/HOL/Auth/Recur.ML Fri Aug 21 15:56:12 1998 +0200 +++ b/src/HOL/Auth/Recur.ML Fri Aug 21 16:14:34 1998 +0200 @@ -9,6 +9,11 @@ Pretty.setdepth 30; +AddEs spies_partsEs; +AddDs [impOfSubs analz_subset_parts]; +AddDs [impOfSubs Fake_parts_insert]; + + (** Possibility properties: traces that reach the end ONE theorem would be more elegant and faster! By induction on a list of agents (no repetitions) @@ -104,8 +109,7 @@ val RA2_analz_spies = Says_imp_spies RS analz.Inj |> standard; -Goal "Says C' B {|Crypt K X, X', RA|} : set evs \ -\ ==> RA : analz (spies evs)"; +Goal "Says C' B {|Crypt K X, X', RA|} : set evs ==> RA : analz (spies evs)"; by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1); qed "RA4_analz_spies"; @@ -121,11 +125,11 @@ (*For proving the easier theorems about X ~: parts (spies evs).*) fun parts_induct_tac i = - etac recur.induct i THEN - forward_tac [RA2_parts_spies] (i+3) THEN - forward_tac [respond_imp_responses] (i+4) THEN - forward_tac [RA4_parts_spies] (i+5) THEN - prove_simple_subgoals_tac i; + EVERY [etac recur.induct i, + forward_tac [RA4_parts_spies] (i+5), + forward_tac [respond_imp_responses] (i+4), + forward_tac [RA2_parts_spies] (i+3), + prove_simple_subgoals_tac i]; (** Theorems of the form X ~: parts (spies evs) imply that NOBODY @@ -136,16 +140,15 @@ Goal "evs : recur ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); -by (ALLGOALS - (asm_simp_tac (simpset() addsimps [parts_insert2, parts_insert_spies]))); +by Auto_tac; (*RA3*) -by (blast_tac (claset() addDs [Key_in_parts_respond]) 1); +by (auto_tac (claset() addDs [Key_in_parts_respond], + simpset() addsimps [parts_insert_spies])); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; Goal "evs : recur ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; -by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); +by Auto_tac; qed "Spy_analz_shrK"; Addsimps [Spy_analz_shrK]; @@ -156,16 +159,15 @@ (** Nobody can have used non-existent keys! **) (*The special case of H={} has the same proof*) -Goal "[| K : keysFor (parts (insert RB H)); (PB,RB,K') : respond evs |] \ +Goal "[| K : keysFor (parts (insert RB H)); RB : responses evs |] \ \ ==> K : range shrK | K : keysFor (parts H)"; by (etac rev_mp 1); -by (etac (respond_imp_responses RS responses.induct) 1); +by (etac responses.induct 1); by Auto_tac; qed_spec_mp "Key_in_keysFor_parts"; -Goal "evs : recur ==> \ -\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; +Goal "evs : recur ==> Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; by (parts_induct_tac 1); (*RA3*) by (blast_tac (claset() addSDs [Key_in_keysFor_parts]) 2); @@ -244,8 +246,7 @@ (*Everything that's hashed is already in past traffic. *) Goal "[| Hash {|Key(shrK A), X|} : parts (spies evs); \ -\ evs : recur; A ~: bad |] \ -\ ==> X : parts (spies evs)"; +\ evs : recur; A ~: bad |] ==> X : parts (spies evs)"; by (etac rev_mp 1); by (parts_induct_tac 1); (*RA3 requires a further induction*) @@ -267,15 +268,14 @@ \ Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (spies evs) \ \ --> B=B' & P=P'"; by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); by (etac responses.induct 3); by (ALLGOALS (simp_tac (simpset() addsimps [all_conj_distrib]))); by (clarify_tac (claset() addSEs partsEs) 1); (*RA1,2: creation of new Nonce. Move assertion into global context*) by (ALLGOALS (expand_case_tac "NA = ?y")); by (REPEAT_FIRST (ares_tac [exI])); -by (REPEAT (blast_tac (claset() addSDs [Hash_imp_body] - addSEs spies_partsEs) 1)); +by (REPEAT (blast_tac (claset() addSDs [Hash_imp_body]) 1)); val lemma = result(); Goalw [HPair_def] @@ -342,10 +342,10 @@ qed "respond_certificate"; -Goal "!!K'. (PB,RB,KXY) : respond evs \ -\ ==> EX A' B'. ALL A B N. \ -\ Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB} \ -\ --> (A'=A & B'=B) | (A'=B & B'=A)"; +Goal "(PB,RB,KXY) : respond evs \ +\ ==> EX A' B'. ALL A B N. \ +\ Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB} \ +\ --> (A'=A & B'=B) | (A'=B & B'=A)"; by (etac respond.induct 1); by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [all_conj_distrib]))); (*Base case*) @@ -354,19 +354,18 @@ by (expand_case_tac "K = KBC" 1); by (dtac respond_Key_in_parts 1); by (blast_tac (claset() addSIs [exI] - addSEs partsEs addDs [Key_in_parts_respond]) 1); by (expand_case_tac "K = KAB" 1); by (REPEAT (ares_tac [exI] 2)); by (ex_strip_tac 1); by (dtac respond_certificate 1); -by (Fast_tac 1); +by (Blast_tac 1); val lemma = result(); Goal "[| Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB}; \ -\ Crypt (shrK A') {|Key K, Agent B', N'|} : parts {RB}; \ -\ (PB,RB,KXY) : respond evs |] \ -\ ==> (A'=A & B'=B) | (A'=B & B'=A)"; +\ Crypt (shrK A') {|Key K, Agent B', N'|} : parts {RB}; \ +\ (PB,RB,KXY) : respond evs |] \ +\ ==> (A'=A & B'=B) | (A'=B & B'=A)"; by (prove_unique_tac lemma 1); qed "unique_session_keys"; @@ -390,11 +389,11 @@ [shrK_in_analz_respond, resp_analz_image_freshK, parts_insert2]))); by (ALLGOALS (simp_tac (simpset() addsimps [ex_disj_distrib]))); (** LEVEL 5 **) -by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1); +by (Blast_tac 1); by (REPEAT_FIRST (resolve_tac [allI, conjI, impI])); by (ALLGOALS Clarify_tac); by (blast_tac (claset() addSDs [resp_analz_insert] - addIs [impOfSubs analz_subset_parts]) 2); + addIs [impOfSubs analz_subset_parts]) 2); by (blast_tac (claset() addSDs [respond_certificate]) 1); by (Asm_full_simp_tac 1); (*by unicity, either B=Aa or B=A', a contradiction if B: bad*) @@ -456,7 +455,7 @@ \ ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) : set evs"; by (etac rev_mp 1); by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); (*RA3*) by (blast_tac (claset() addSDs [Hash_in_parts_respond]) 1); qed_spec_mp "Hash_auth_sender"; @@ -473,7 +472,7 @@ \ Crypt (shrK A) Y : parts {RC}"; by (etac rev_mp 1); by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); (*RA4*) by (Blast_tac 4); (*RA3*) diff -r 7e046ef59fe2 -r bd539b72d484 src/HOL/Auth/Recur.thy --- a/src/HOL/Auth/Recur.thy Fri Aug 21 15:56:12 1998 +0200 +++ b/src/HOL/Auth/Recur.thy Fri Aug 21 16:14:34 1998 +0200 @@ -92,7 +92,17 @@ RA|} : set evs4 |] ==> Says B A RA # evs4 : recur" -(**No "oops" message can easily be expressed. Each session key is - associated--in two separate messages--with two nonces. -***) end + + (*No "oops" message can easily be expressed. Each session key is + associated--in two separate messages--with two nonces. This is + one try, but it isn't that useful. Re domino attack, note that + Recur.ML proves that each session key is secure provided the two + peers are, even if there are compromised agents elsewhere in + the chain. Oops cases proved using parts_cut, Key_in_keysFor_parts, + etc. + + Oops "[| evso: recur; Says Server B RB : set evso; + RB : responses evs'; Key K : parts {RB} |] + ==> Notes Spy {|Key K, RB|} # evso : recur" + *) diff -r 7e046ef59fe2 -r bd539b72d484 src/HOL/Auth/TLS.ML --- a/src/HOL/Auth/TLS.ML Fri Aug 21 15:56:12 1998 +0200 +++ b/src/HOL/Auth/TLS.ML Fri Aug 21 16:14:34 1998 +0200 @@ -163,8 +163,7 @@ little point in doing so: the loss of their private keys is a worse breach of security.*) Goalw [certificate_def] - "[| certificate B KB : parts (spies evs); evs : tls |] \ -\ ==> pubK B = KB"; + "[| certificate B KB : parts (spies evs); evs : tls |] ==> pubK B = KB"; by (etac rev_mp 1); by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); @@ -193,7 +192,7 @@ (*** Properties of items found in Notes ***) Goal "[| Notes A {|Agent B, X|} : set evs; evs : tls |] \ -\ ==> Crypt (pubK B) X : parts (spies evs)"; +\ ==> Crypt (pubK B) X : parts (spies evs)"; by (etac rev_mp 1); by (analz_induct_tac 1); by (blast_tac (claset() addIs [parts_insertI]) 1); @@ -201,8 +200,8 @@ (*C may be either A or B*) Goal "[| Notes C {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} : set evs; \ -\ evs : tls \ -\ |] ==> Crypt (pubK B) (Nonce PMS) : parts (spies evs)"; +\ evs : tls |] \ +\ ==> Crypt (pubK B) (Nonce PMS) : parts (spies evs)"; by (etac rev_mp 1); by (parts_induct_tac 1); by (ALLGOALS Clarify_tac); @@ -215,8 +214,8 @@ (*Compared with the theorem above, both premise and conclusion are stronger*) Goal "[| Notes A {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} : set evs;\ -\ evs : tls \ -\ |] ==> Notes A {|Agent B, Nonce PMS|} : set evs"; +\ evs : tls |] \ +\ ==> Notes A {|Agent B, Nonce PMS|} : set evs"; by (etac rev_mp 1); by (parts_induct_tac 1); (*ServerAccepts*) @@ -230,7 +229,7 @@ Goal "[| X : parts (spies evs); \ \ X = Crypt (priK A) (Hash{|nb, Agent B, pms|}); \ \ evs : tls; A ~: bad |] \ -\ ==> Says A B X : set evs"; +\ ==> Says A B X : set evs"; by (etac rev_mp 1); by (hyp_subst_tac 1); by (parts_induct_tac 1); @@ -242,7 +241,7 @@ \ X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|}); \ \ certificate A KA : parts (spies evs); \ \ evs : tls; A ~: bad |] \ -\ ==> Says A B X : set evs"; +\ ==> Says A B X : set evs"; by (blast_tac (claset() addSDs [certificate_valid] addSIs [lemma]) 1); qed "TrustCertVerify"; @@ -275,12 +274,13 @@ Addsimps [no_Notes_A_PRF]; -Goal "[| Nonce (PRF (PMS,NA,NB)) : parts (spies evs); \ -\ evs : tls |] \ -\ ==> Nonce PMS : parts (spies evs)"; +Goal "[| Nonce (PRF (PMS,NA,NB)) : parts (spies evs); evs : tls |] \ +\ ==> Nonce PMS : parts (spies evs)"; by (etac rev_mp 1); by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); +(*SpyKeys*) +by (blast_tac (claset() addDs [impOfSubs analz_subset_parts]) 1); (*Six others, all trivial or by freshness*) by (REPEAT (blast_tac (claset() addSDs [Notes_Crypt_parts_spies] addSEs spies_partsEs) 1)); @@ -321,9 +321,8 @@ **) (*In A's internal Note, PMS determines A and B.*) -Goal "evs : tls \ -\ ==> EX A' B'. ALL A B. \ -\ Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'"; +Goal "evs : tls ==> EX A' B'. ALL A B. \ +\ Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'"; by (parts_induct_tac 1); by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1); (*ClientKeyExch: if PMS is fresh, then it can't appear in Notes A X.*) @@ -344,9 +343,9 @@ (*Key compromise lemma needed to prove analz_image_keys. No collection of keys can help the spy get new private keys.*) -Goal "evs : tls ==> \ -\ ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \ -\ (priK B : KK | B : bad)"; +Goal "evs : tls \ +\ ==> ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \ +\ (priK B : KK | B : bad)"; by (etac tls.induct 1); by (ALLGOALS (asm_simp_tac (analz_image_keys_ss @@ -416,7 +415,7 @@ by (hyp_subst_tac 1); by (analz_induct_tac 1); (*SpyKeys*) -by (blast_tac (claset() addSEs spies_partsEs) 3); +by (blast_tac (claset() addDs [impOfSubs analz_subset_parts]) 3); (*Fake*) by (Fake_parts_insert_tac 2); (** LEVEL 6 **) @@ -512,9 +511,9 @@ (*If A created PMS then nobody other than the Spy would send a message using a clientK generated from that PMS.*) Goal "[| evs : tls; A' ~= Spy |] \ -\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ -\ Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs --> \ -\ A = A'"; +\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ +\ Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs --> \ +\ A = A'"; by (analz_induct_tac 1); (*8 seconds*) by (ALLGOALS Clarify_tac); (*ClientFinished, ClientResume: by unicity of PMS*) @@ -531,9 +530,9 @@ (*If A created PMS and has not leaked her clientK to the Spy, then nobody has.*) Goal "evs : tls \ -\ ==> Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \ -\ Notes A {|Agent B, Nonce PMS|} : set evs --> \ -\ (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) "; +\ ==> Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \ +\ Notes A {|Agent B, Nonce PMS|} : set evs --> \ +\ (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs)"; by (etac tls.induct 1); (*This roundabout proof sequence avoids looping in simplification*) by (ALLGOALS Simp_tac); @@ -554,9 +553,9 @@ (*If A created PMS for B, then nobody other than B or the Spy would send a message using a serverK generated from that PMS.*) Goal "[| evs : tls; A ~: bad; B ~: bad; B' ~= Spy |] \ -\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ -\ Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs --> \ -\ B = B'"; +\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ +\ Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs --> \ +\ B = B'"; by (analz_induct_tac 1); (*9 seconds*) by (ALLGOALS Clarify_tac); (*ServerResume, ServerFinished: by unicity of PMS*) @@ -690,10 +689,10 @@ ***) Goal "[| M = PRF(PMS,NA,NB); evs : tls; A ~: bad; B ~: bad |] \ -\ ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs) --> \ -\ Notes A {|Agent B, Nonce PMS|} : set evs --> \ -\ Crypt (clientK(Na,Nb,M)) Y : parts (spies evs) --> \ -\ Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs"; +\ ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs) --> \ +\ Notes A {|Agent B, Nonce PMS|} : set evs --> \ +\ Crypt (clientK(Na,Nb,M)) Y : parts (spies evs) --> \ +\ Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs"; by (hyp_subst_tac 1); by (analz_induct_tac 1); (*15 seconds*) by (ALLGOALS Clarify_tac); @@ -716,7 +715,7 @@ \ Notes A {|Agent B, Nonce PMS|} : set evs; \ \ Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs; \ \ evs : tls; A ~: bad; B ~: bad |] \ -\ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs"; +\ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs"; by (blast_tac (claset() addIs [lemma] addEs [clientK_Oops_ALL RSN(2, rev_notE)]) 1); qed "TrustClientMsg"; @@ -733,8 +732,8 @@ \ certificate A KA : parts (spies evs); \ \ Says A'' B (Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}))\ \ : set evs; \ -\ evs : tls; A ~: bad; B ~: bad |] \ -\ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs"; +\ evs : tls; A ~: bad; B ~: bad |] \ +\ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs"; by (blast_tac (claset() addSIs [TrustClientMsg, UseCertVerify] addDs [Says_imp_spies RS parts.Inj]) 1); qed "AuthClientFinished"; diff -r 7e046ef59fe2 -r bd539b72d484 src/HOL/Auth/TLS.thy --- a/src/HOL/Auth/TLS.thy Fri Aug 21 15:56:12 1998 +0200 +++ b/src/HOL/Auth/TLS.thy Fri Aug 21 16:14:34 1998 +0200 @@ -88,7 +88,7 @@ SpyKeys (*The spy may apply PRF & sessionK to available nonces*) "[| evsSK: tls; - Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evsSK |] + {Nonce NA, Nonce NB, Nonce M} <= analz (spies evsSK) |] ==> Notes Spy {| Nonce (PRF(M,NA,NB)), Key (sessionK((NA,NB,M),b)) |} # evsSK : tls" diff -r 7e046ef59fe2 -r bd539b72d484 src/HOL/Auth/Yahalom.thy --- a/src/HOL/Auth/Yahalom.thy Fri Aug 21 15:56:12 1998 +0200 +++ b/src/HOL/Auth/Yahalom.thy Fri Aug 21 16:14:34 1998 +0200 @@ -60,7 +60,7 @@ (*This message models possible leaks of session keys. The Nonces identify the protocol run. Quoting Server here ensures they are correct.*) - Oops "[| evso: yahalom; A ~= Spy; + Oops "[| evso: yahalom; Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|} : set evso |] diff -r 7e046ef59fe2 -r bd539b72d484 src/HOL/Auth/Yahalom2.thy --- a/src/HOL/Auth/Yahalom2.thy Fri Aug 21 15:56:12 1998 +0200 +++ b/src/HOL/Auth/Yahalom2.thy Fri Aug 21 16:14:34 1998 +0200 @@ -64,7 +64,7 @@ (*This message models possible leaks of session keys. The nonces identify the protocol run. Quoting Server here ensures they are correct. *) - Oops "[| evso: yahalom; A ~= Spy; + Oops "[| evso: yahalom; Says Server A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} : set evso |]