# HG changeset patch # User paulson # Date 984556255 -3600 # Node ID bb01189f0565f5bc3da0092dae7a241b0b69dc46 # Parent 881222d487778b407f846b0d1929a4f700c9c125 minor tuning diff -r 881222d48777 -r bb01189f0565 src/HOL/Auth/KerberosIV.ML --- a/src/HOL/Auth/KerberosIV.ML Tue Mar 13 18:35:48 2001 +0100 +++ b/src/HOL/Auth/KerberosIV.ML Wed Mar 14 08:50:55 2001 +0100 @@ -185,8 +185,8 @@ qed_spec_mp "new_keys_not_used"; Addsimps [new_keys_not_used]; -(*Earlier, \\protocol proofs declared this theorem. - But Yahalom and Kerberos IV are the only ones that need it!*) +(*Earlier, all protocol proofs declared this theorem. + But few of them actually need it! (Another is Yahalom) *) bind_thm ("new_keys_not_analzd", [analz_subset_parts RS keysFor_mono, new_keys_not_used] MRS contra_subsetD); @@ -492,7 +492,7 @@ by (blast_tac (claset() addSEs spies_partsEs) 1); qed "Serv_fresh_not_KeyCryptKey"; -Goalw [KeyCryptKey_def] +Goal "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, tk|}\ \ \\ parts (spies evs); evs \\ kerberos |] \ \ ==> ~ KeyCryptKey K AuthKey evs"; @@ -501,24 +501,23 @@ (*K4*) by (blast_tac (claset() addEs spies_partsEs) 3); (*K2: by freshness*) +by (asm_full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 2); by (blast_tac (claset() addEs spies_partsEs) 2); by (Fake_parts_insert_tac 1); qed "AuthKey_not_KeyCryptKey"; (*A secure serverkey cannot have been used to encrypt others*) -Goalw [KeyCryptKey_def] - "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, tt|} \ -\ \\ parts (spies evs); \ -\ Key ServKey \\ analz (spies evs); \ -\ B \\ Tgs; evs \\ kerberos |] \ -\ ==> ~ KeyCryptKey ServKey K evs"; +Goal + "[| Crypt (shrK B) {|Agent A, Agent B, Key SK, tt|} \\ parts (spies evs); \ +\ Key SK \\ analz (spies evs); \ +\ B \\ Tgs; evs \\ kerberos |] \ +\ ==> ~ KeyCryptKey SK K evs"; by (etac rev_mp 1); by (etac rev_mp 1); by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); (*K4 splits into distinct subcases*) -by (Step_tac 1); -by (ALLGOALS Asm_full_simp_tac); +by Auto_tac; (*ServKey can't have been enclosed in two certificates*) by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj] addSEs [MPair_parts] @@ -526,7 +525,7 @@ (*ServKey is fresh and so could not have been used, by new_keys_not_used*) by (force_tac (claset() addSDs [Says_imp_spies RS parts.Inj, Crypt_imp_invKey_keysFor], - simpset()) 2); + simpset() addsimps [KeyCryptKey_def]) 2); (*Others by freshness*) by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1)); qed "ServKey_not_KeyCryptKey"; @@ -610,11 +609,6 @@ REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE, exE] ORELSE' hyp_subst_tac)]; -Goal "[| KK <= -(range shrK); Key K \\ analz (spies evs); evs \\ kerberos |] \ -\ ==> Key K \\ analz (Key ` KK Un spies evs)"; -by (blast_tac (claset() addDs [impOfSubs analz_mono]) 1); -qed "analz_mono_KK"; - (*For the Oops2 case of the next theorem*) Goal "[| evs \\ kerberos; \ \ Says Tgs A (Crypt AuthKey \ diff -r 881222d48777 -r bb01189f0565 src/HOL/Auth/OtwayRees.ML --- a/src/HOL/Auth/OtwayRees.ML Tue Mar 13 18:35:48 2001 +0100 +++ b/src/HOL/Auth/OtwayRees.ML Wed Mar 14 08:50:55 2001 +0100 @@ -17,10 +17,10 @@ (*A "possibility property": there are traces that reach the end*) -Goal "B ~= Server \ +Goal "B \\ Server \ \ ==> \\NA K. \\evs \\ otway. \ \ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \ -\ : set evs"; +\ \\ set evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); by (rtac (otway.Nil RS otway.OR1 RS otway.Reception RS @@ -29,14 +29,14 @@ by possibility_tac; result(); -Goal "[| Gets B X : set evs; evs : otway |] ==> \\A. Says A B X : set evs"; +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"; +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]; @@ -46,18 +46,18 @@ (** 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)"; +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)"; +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)"; +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"; @@ -79,13 +79,13 @@ 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)"; +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)"; +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]; @@ -98,8 +98,8 @@ (*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 |] \ +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); @@ -119,8 +119,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) + Key K \\ analz (insert (Key KAB) (knows Spy evs)) ==> + Key K \\ analz (knows Spy evs) A more general formula must be proved inductively. ****) @@ -129,9 +129,9 @@ (** 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))"; +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])); @@ -142,18 +142,18 @@ 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))"; +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'"; +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); @@ -166,21 +166,21 @@ (**** 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) --> \ +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"; +\ \\ 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 |] \ +\ 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"; +\ \\ set evs"; by (blast_tac (claset() addDs [Crypt_imp_OR1]) 1); qed"Crypt_imp_OR1_Gets"; @@ -189,7 +189,7 @@ 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 |] \ +\ evs \\ otway; A \\ bad |] \ \ ==> B = C"; by (etac rev_mp 1); by (etac rev_mp 1); @@ -202,8 +202,8 @@ (*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) --> \ +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); @@ -214,14 +214,14 @@ (*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 |] \ +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) \ +\ 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)"; +\ 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.*) @@ -238,14 +238,14 @@ 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 |] \ +\ 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"; +\ \\ set evs"; by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1); qed "A_trusts_OR4"; @@ -254,10 +254,10 @@ 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 |] \ +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 --> \ +\ 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); @@ -278,9 +278,9 @@ Goal "[| Says Server B \ \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ -\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \ +\ Crypt (shrK B) {|NB, Key K|}|} \\ set evs; \ \ Notes Spy {|NA, NB, Key K|} \\ set evs; \ -\ A \\ bad; B \\ bad; evs : otway |] \ +\ 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"; @@ -289,10 +289,10 @@ (*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; \ +\ 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 |] \ +\ 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"; @@ -303,12 +303,12 @@ (*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 |] \ +\ \\ 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"; +\ \\ set evs"; by (etac rev_mp 1); by (parts_induct_tac 1); by (ALLGOALS Blast_tac); @@ -317,9 +317,9 @@ (** 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 |] \ +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); @@ -330,16 +330,16 @@ (*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) \ +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 \ +\ \\ set evs \ \ --> Says Server B \ \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ \ Crypt (shrK B) {|NB, Key K|}|} \ -\ : set evs)"; +\ \\ set evs)"; by (asm_full_simp_tac (simpset() addsimps []) 1); by (parts_induct_tac 1); by (Blast_tac 1); @@ -357,14 +357,14 @@ 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 |] \ +\ \\ 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"; +\ \\ set evs"; by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1); qed "B_trusts_OR3"; @@ -372,10 +372,10 @@ (*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; \ +\ \\ 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 |] \ +\ 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"; @@ -383,11 +383,11 @@ Goal "[| Says Server B \ \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ -\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \ -\ B \\ bad; evs : otway |] \ +\ 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"; +\ \\ set evs"; by (etac rev_mp 1); by (etac otway.induct 1); by (ALLGOALS Asm_simp_tac); @@ -399,13 +399,13 @@ (*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; \ +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 |] \ +\ 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"; +\ \\ 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 881222d48777 -r bb01189f0565 src/HOL/Auth/OtwayRees_AN.ML --- a/src/HOL/Auth/OtwayRees_AN.ML Tue Mar 13 18:35:48 2001 +0100 +++ b/src/HOL/Auth/OtwayRees_AN.ML Wed Mar 14 08:50:55 2001 +0100 @@ -17,7 +17,7 @@ (*A "possibility property": there are traces that reach the end*) -Goal "B ~= Server \ +Goal "B \\ Server \ \ ==> \\K. \\NA. \\evs \\ otway. \ \ Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \ \ \\ set evs"; @@ -112,8 +112,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) + Key K \\ analz (insert (Key KAB) (knows Spy evs)) ==> + Key K \\ analz (knows Spy evs) A more general formula must be proved inductively. ****) @@ -168,7 +168,7 @@ (**** Authenticity properties relating to NA ****) (*If the encrypted message appears then it originated with the Server!*) -Goal "[| A \\ bad; A ~= B; evs \\ otway |] \ +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|}, \ @@ -186,7 +186,7 @@ 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 |] \ +\ 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|}|} \ @@ -239,7 +239,7 @@ 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 |] \ +\ 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"; @@ -248,7 +248,7 @@ (**** Authenticity properties relating to NB ****) (*If the encrypted message appears then it originated with the Server!*) -Goal "[| B \\ bad; A ~= B; evs \\ otway |] \ +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|}, \ @@ -266,7 +266,7 @@ 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 |] \ +\ 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|}|} \ @@ -279,7 +279,7 @@ 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 |] \ +\ 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 881222d48777 -r bb01189f0565 src/HOL/Auth/OtwayRees_Bad.ML --- a/src/HOL/Auth/OtwayRees_Bad.ML Tue Mar 13 18:35:48 2001 +0100 +++ b/src/HOL/Auth/OtwayRees_Bad.ML Wed Mar 14 08:50:55 2001 +0100 @@ -19,7 +19,7 @@ AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; (*A "possibility property": there are traces that reach the end*) -Goal "B ~= Server \ +Goal "B \\ Server \ \ ==> \\K. \\NA. \\evs \\ otway. \ \ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \ \ \\ set evs"; @@ -207,9 +207,9 @@ (*** 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 + 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 |] \ +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"; @@ -220,10 +220,10 @@ (*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*) + 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 |] \ +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|}|} \ diff -r 881222d48777 -r bb01189f0565 src/HOL/Auth/Yahalom.ML --- a/src/HOL/Auth/Yahalom.ML Tue Mar 13 18:35:48 2001 +0100 +++ b/src/HOL/Auth/Yahalom.ML Wed Mar 14 08:50:55 2001 +0100 @@ -107,8 +107,8 @@ qed_spec_mp "new_keys_not_used"; Addsimps [new_keys_not_used]; -(*Earlier, \\protocol proofs declared this theorem. - But Yahalom and Kerberos IV are the only ones that need it!*) +(*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);