# HG changeset patch # User paulson # Date 899394491 -7200 # Node ID c729d4c299c1009816d4eb9d08a92ef5e126f68f # Parent c4da11bb0592da27a694173fb468fc1fb0e677f9 Deleted leading parameters thanks to new Goal command diff -r c4da11bb0592 -r c729d4c299c1 src/HOL/Auth/Event.ML --- a/src/HOL/Auth/Event.ML Thu Jul 02 17:27:35 1998 +0200 +++ b/src/HOL/Auth/Event.ML Thu Jul 02 17:48:11 1998 +0200 @@ -22,8 +22,7 @@ read_instantiate_sg (sign_of thy) [("H", "spies evs")]); -Goal - "P(event_case sf nf ev) = \ +Goal "P(event_case sf nf ev) = \ \ ((ALL A B X. ev = Says A B X --> P(sf A B X)) & \ \ (ALL A X. ev = Notes A X --> P(nf A X)))"; by (induct_tac "ev" 1); diff -r c4da11bb0592 -r c729d4c299c1 src/HOL/Auth/Kerberos_BAN.ML --- a/src/HOL/Auth/Kerberos_BAN.ML Thu Jul 02 17:27:35 1998 +0200 +++ b/src/HOL/Auth/Kerberos_BAN.ML Thu Jul 02 17:48:11 1998 +0200 @@ -33,11 +33,10 @@ (*A "possibility property": there are traces that reach the end.*) -Goal - "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ -\ ==> EX Timestamp K. EX evs: kerberos_ban. \ -\ Says B A (Crypt K (Number Timestamp)) \ -\ : set evs"; +Goal "[| A ~= B; A ~= Server; B ~= Server |] \ +\ ==> EX Timestamp K. EX evs: kerberos_ban. \ +\ Says B A (Crypt K (Number Timestamp)) \ +\ : set evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); by (rtac (kerberos_ban.Nil RS kerberos_ban.Kb1 RS kerberos_ban.Kb2 RS kerberos_ban.Kb3 RS kerberos_ban.Kb4) 2); @@ -52,7 +51,7 @@ (**** Inductive proofs about kerberos_ban ****) (*Nobody sends themselves messages*) -Goal "!!evs. evs : kerberos_ban ==> ALL A X. Says A A X ~: set evs"; +Goal "evs : kerberos_ban ==> ALL A X. Says A A X ~: set evs"; by (etac kerberos_ban.induct 1); by Auto_tac; qed_spec_mp "not_Says_to_self"; @@ -61,14 +60,13 @@ (*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*) -Goal "!!evs. Says S A (Crypt KA {|Timestamp, B, K, X|}) : set evs \ -\ ==> X : parts (spies evs)"; +Goal "Says S A (Crypt KA {|Timestamp, B, K, X|}) : set evs \ +\ ==> X : parts (spies evs)"; by (Blast_tac 1); qed "Kb3_msg_in_parts_spies"; -Goal - "!!evs. Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) : set evs \ -\ ==> K : parts (spies evs)"; +Goal "Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) : set evs \ +\ ==> K : parts (spies evs)"; by (Blast_tac 1); qed "Oops_parts_spies"; @@ -81,22 +79,20 @@ (*Spy never sees another agent's shared key! (unless it's bad at start)*) -Goal -"!!evs. evs : kerberos_ban ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; +Goal "evs : kerberos_ban ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; by (parts_induct_tac 1); by (ALLGOALS Blast_tac); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; -Goal -"!!evs. evs : kerberos_ban ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; +Goal "evs : kerberos_ban ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; by Auto_tac; qed "Spy_analz_shrK"; Addsimps [Spy_analz_shrK]; -Goal "!!A. [| Key (shrK A) : parts (spies evs); \ -\ evs : kerberos_ban |] ==> A:bad"; +Goal "[| Key (shrK A) : parts (spies evs); \ +\ evs : kerberos_ban |] ==> A:bad"; by (blast_tac (claset() addDs [Spy_see_shrK]) 1); qed "Spy_see_shrK_D"; @@ -105,8 +101,8 @@ (*Nobody can have used non-existent keys!*) -Goal "!!evs. evs : kerberos_ban ==> \ -\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; +Goal "evs : kerberos_ban ==> \ +\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; by (parts_induct_tac 1); (*Fake*) by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); @@ -124,12 +120,11 @@ (** Lemmas concerning the form of items passed in messages **) (*Describes the form of K, X and K' when the Server sends this message.*) -Goal - "!!evs. [| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|}) \ -\ : set evs; evs : kerberos_ban |] \ -\ ==> K ~: range shrK & \ -\ X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}) & \ -\ K' = shrK A"; +Goal "[| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|}) \ +\ : set evs; evs : kerberos_ban |] \ +\ ==> K ~: range shrK & \ +\ X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}) & \ +\ K' = shrK A"; by (etac rev_mp 1); by (etac kerberos_ban.induct 1); by Auto_tac; @@ -141,12 +136,11 @@ This shows implicitly the FRESHNESS OF THE SESSION KEY to A *) -Goal - "!!evs. [| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} \ -\ : parts (spies evs); \ -\ A ~: bad; evs : kerberos_ban |] \ -\ ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \ -\ : set evs"; +Goal "[| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} \ +\ : parts (spies evs); \ +\ A ~: bad; evs : kerberos_ban |] \ +\ ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \ +\ : set evs"; by (etac rev_mp 1); by (parts_induct_tac 1); by (Blast_tac 1); @@ -155,13 +149,12 @@ (*If the TICKET appears then it originated with the Server*) (*FRESHNESS OF THE SESSION KEY to B*) -Goal - "!!evs. [| Crypt (shrK B) {|Number Ts, Agent A, Key K|} : parts (spies evs); \ -\ B ~: bad; evs : kerberos_ban |] \ -\ ==> Says Server A \ -\ (Crypt (shrK A) {|Number Ts, Agent B, Key K, \ -\ Crypt (shrK B) {|Number Ts, Agent A, Key K|}|}) \ -\ : set evs"; +Goal "[| Crypt (shrK B) {|Number Ts, Agent A, Key K|} : parts (spies evs); \ +\ B ~: bad; evs : kerberos_ban |] \ +\ ==> Says Server A \ +\ (Crypt (shrK A) {|Number Ts, Agent B, Key K, \ +\ Crypt (shrK B) {|Number Ts, Agent A, Key K|}|}) \ +\ : set evs"; by (etac rev_mp 1); by (parts_induct_tac 1); by (Blast_tac 1); @@ -171,12 +164,11 @@ (*EITHER describes the form of X when the following message is sent, OR reduces it to the Fake case. Use Says_Server_message_form if applicable.*) -Goal - "!!evs. [| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \ -\ : set evs; \ -\ evs : kerberos_ban |] \ -\ ==> (K ~: range shrK & X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}))\ -\ | X : analz (spies evs)"; +Goal "[| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \ +\ : set evs; \ +\ evs : kerberos_ban |] \ +\==> (K ~: range shrK & X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}))\ +\ | X : analz (spies evs)"; by (case_tac "A : bad" 1); by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj] addss (simpset())) 1); @@ -206,11 +198,10 @@ (** Session keys are not used to encrypt other session keys **) -Goal - "!!evs. evs : kerberos_ban ==> \ +Goal "evs : kerberos_ban ==> \ \ ALL K KK. KK <= Compl (range shrK) --> \ -\ (Key K : analz (Key``KK Un (spies evs))) = \ -\ (K : KK | Key K : analz (spies evs))"; +\ (Key K : analz (Key``KK Un (spies evs))) = \ +\ (K : KK | Key K : analz (spies evs))"; by (etac kerberos_ban.induct 1); by analz_spies_tac; by (REPEAT_FIRST (resolve_tac [allI, impI])); @@ -222,22 +213,20 @@ qed_spec_mp "analz_image_freshK"; -Goal - "!!evs. [| evs : kerberos_ban; KAB ~: range shrK |] ==> \ -\ Key K : analz (insert (Key KAB) (spies evs)) = \ -\ (K = KAB | Key K : analz (spies evs))"; +Goal "[| evs : kerberos_ban; 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"; (** The session key K uniquely identifies the message **) -Goal - "!!evs. evs : kerberos_ban ==> \ -\ EX A' Ts' B' X'. ALL A Ts B X. \ -\ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \ -\ : set evs \ -\ --> A=A' & Ts=Ts' & B=B' & X=X'"; +Goal "evs : kerberos_ban ==> \ +\ EX A' Ts' B' X'. ALL A Ts B X. \ +\ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \ +\ : set evs \ +\ --> A=A' & Ts=Ts' & B=B' & X=X'"; by (etac kerberos_ban.induct 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); by Safe_tac; @@ -248,12 +237,11 @@ val lemma = result(); (*In messages of this form, the session key uniquely identifies the rest*) -Goal - "!!evs. [| Says Server A \ -\ (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) : set evs; \ -\ Says Server A' \ -\ (Crypt (shrK A') {|Number Ts', Agent B', Key K, X'|}) : set evs;\ -\ evs : kerberos_ban |] ==> A=A' & Ts=Ts' & B=B' & X = X'"; +Goal "[| Says Server A \ +\ (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) : set evs; \ +\ Says Server A' \ +\ (Crypt (shrK A') {|Number Ts', Agent B', Key K, X'|}) : set evs;\ +\ evs : kerberos_ban |] ==> A=A' & Ts=Ts' & B=B' & X = X'"; by (prove_unique_tac lemma 1); qed "unique_session_keys"; @@ -262,13 +250,12 @@ if the spy could see it! **) -Goal - "!!evs. [| A ~: bad; B ~: bad; evs : kerberos_ban |] \ -\ ==> Says Server A \ -\ (Crypt (shrK A) {|Number Ts, Agent B, Key K, \ -\ Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})\ -\ : set evs --> \ -\ Key K : analz (spies evs) --> Expired Ts evs"; +Goal "[| A ~: bad; B ~: bad; evs : kerberos_ban |] \ +\ ==> Says Server A \ +\ (Crypt (shrK A) {|Number Ts, Agent B, Key K, \ +\ Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})\ +\ : set evs --> \ +\ Key K : analz (spies evs) --> Expired Ts evs"; by (etac kerberos_ban.induct 1); by analz_spies_tac; by (ALLGOALS @@ -294,12 +281,11 @@ Spy does not see the keys sent in msg Kb2 as long as they have NOT EXPIRED **) -Goal - "!!evs. [| Says Server A \ -\ (Crypt K' {|Number T, Agent B, Key K, X|}) : set evs; \ -\ ~ Expired T evs; \ -\ A ~: bad; B ~: bad; evs : kerberos_ban \ -\ |] ==> Key K ~: analz (spies evs)"; +Goal "[| Says Server A \ +\ (Crypt K' {|Number T, Agent B, Key K, X|}) : set evs; \ +\ ~ Expired T evs; \ +\ A ~: bad; B ~: bad; evs : kerberos_ban \ +\ |] ==> Key K ~: analz (spies evs)"; by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); by (Clarify_tac 1); (*prevents PROOF FAILED*) by (blast_tac (claset() addSEs [lemma]) 1); @@ -312,35 +298,32 @@ (** CONFIDENTIALITY for ALICE: **) (** Also A_trusts_K_by_Kb2 RS Confidentiality_S **) -Goal -"!!evs. [| Crypt (shrK A) {|Number T, Agent B, Key K, X|} : parts (spies evs);\ -\ ~ Expired T evs; \ -\ A ~: bad; B ~: bad; evs : kerberos_ban \ -\ |] ==> Key K ~: analz (spies evs)"; +Goal "[| Crypt (shrK A) {|Number T, Agent B, Key K, X|} : parts (spies evs);\ +\ ~ Expired T evs; \ +\ A ~: bad; B ~: bad; evs : kerberos_ban \ +\ |] ==> Key K ~: analz (spies evs)"; by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2, Confidentiality_S]) 1); qed "Confidentiality_A"; (** CONFIDENTIALITY for BOB: **) (** Also B_trusts_K_by_Kb3 RS Confidentiality_S **) -Goal -"!!evs. [| Crypt (shrK B) {|Number Tk, Agent A, Key K|} \ -\ : parts (spies evs); \ -\ ~ Expired Tk evs; \ -\ A ~: bad; B ~: bad; evs : kerberos_ban \ -\ |] ==> Key K ~: analz (spies evs)"; +Goal "[| Crypt (shrK B) {|Number Tk, Agent A, Key K|} \ +\ : parts (spies evs); \ +\ ~ Expired Tk evs; \ +\ A ~: bad; B ~: bad; evs : kerberos_ban \ +\ |] ==> Key K ~: analz (spies evs)"; by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3, Confidentiality_S]) 1); qed "Confidentiality_B"; -Goal - "!!evs. [| B ~: bad; evs : kerberos_ban |] \ -\ ==> Key K ~: analz (spies evs) --> \ -\ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \ -\ : set evs --> \ -\ Crypt K (Number Ta) : parts (spies evs) --> \ -\ Says B A (Crypt K (Number Ta)) : set evs"; +Goal "[| B ~: bad; evs : kerberos_ban |] \ +\ ==> Key K ~: analz (spies evs) --> \ +\ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \ +\ : set evs --> \ +\ Crypt K (Number Ta) : parts (spies evs) --> \ +\ Says B A (Crypt K (Number Ta)) : set evs"; by (etac kerberos_ban.induct 1); by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); by (dtac Kb3_msg_in_parts_spies 5); @@ -367,27 +350,25 @@ (*AUTHENTICATION OF B TO A*) -Goal - "!!evs. [| Crypt K (Number Ta) : parts (spies evs); \ -\ Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} \ -\ : parts (spies evs); \ -\ ~ Expired Ts evs; \ -\ A ~: bad; B ~: bad; evs : kerberos_ban |] \ -\ ==> Says B A (Crypt K (Number Ta)) : set evs"; +Goal "[| Crypt K (Number Ta) : parts (spies evs); \ +\ Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} \ +\ : parts (spies evs); \ +\ ~ Expired Ts evs; \ +\ A ~: bad; B ~: bad; evs : kerberos_ban |] \ +\ ==> Says B A (Crypt K (Number Ta)) : set evs"; by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2] addSIs [lemma_B RS mp RS mp RS mp] addSEs [Confidentiality_S RSN (2,rev_notE)]) 1); qed "Authentication_B"; -Goal - "!!evs. [| A ~: bad; B ~: bad; evs : kerberos_ban |] ==> \ -\ Key K ~: analz (spies evs) --> \ -\ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \ -\ : set evs --> \ -\ Crypt K {|Agent A, Number Ta|} : parts (spies evs) -->\ -\ Says A B {|X, Crypt K {|Agent A, Number Ta|}|} \ -\ : set evs"; +Goal "[| A ~: bad; B ~: bad; evs : kerberos_ban |] ==> \ +\ Key K ~: analz (spies evs) --> \ +\ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \ +\ : set evs --> \ +\ Crypt K {|Agent A, Number Ta|} : parts (spies evs) -->\ +\ Says A B {|X, Crypt K {|Agent A, Number Ta|}|} \ +\ : set evs"; by (etac kerberos_ban.induct 1); by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); by (forward_tac [Kb3_msg_in_parts_spies] 5); @@ -404,14 +385,13 @@ (*AUTHENTICATION OF A TO B*) -Goal - "!!evs. [| Crypt K {|Agent A, Number Ta|} : parts (spies evs); \ -\ Crypt (shrK B) {|Number Ts, Agent A, Key K|} \ -\ : parts (spies evs); \ -\ ~ Expired Ts evs; \ -\ A ~: bad; B ~: bad; evs : kerberos_ban |] \ -\ ==> Says A B {|Crypt (shrK B) {|Number Ts, Agent A, Key K|}, \ -\ Crypt K {|Agent A, Number Ta|}|} : set evs"; +Goal "[| Crypt K {|Agent A, Number Ta|} : parts (spies evs); \ +\ Crypt (shrK B) {|Number Ts, Agent A, Key K|} \ +\ : parts (spies evs); \ +\ ~ Expired Ts evs; \ +\ A ~: bad; B ~: bad; evs : kerberos_ban |] \ +\ ==> Says A B {|Crypt (shrK B) {|Number Ts, Agent A, Key K|}, \ +\ Crypt K {|Agent A, Number Ta|}|} : set evs"; by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3] addSIs [lemma_A RS mp RS mp RS mp] addSEs [Confidentiality_S RSN (2,rev_notE)]) 1); diff -r c4da11bb0592 -r c729d4c299c1 src/HOL/Auth/Message.ML --- a/src/HOL/Auth/Message.ML Thu Jul 02 17:27:35 1998 +0200 +++ b/src/HOL/Auth/Message.ML Thu Jul 02 17:48:11 1998 +0200 @@ -60,7 +60,7 @@ qed "keysFor_UN"; (*Monotonicity*) -Goalw [keysFor_def] "!!G H. G<=H ==> keysFor(G) <= keysFor(H)"; +Goalw [keysFor_def] "G<=H ==> keysFor(G) <= keysFor(H)"; by (Blast_tac 1); qed "keysFor_mono"; @@ -105,7 +105,7 @@ qed "keysFor_image_Key"; Addsimps [keysFor_image_Key]; -Goalw [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H"; +Goalw [keysFor_def] "Crypt K X : H ==> invKey K : keysFor H"; by (Blast_tac 1); qed "Crypt_imp_invKey_keysFor"; @@ -135,7 +135,7 @@ qed "parts_increasing"; (*Monotonicity*) -Goalw parts.defs "!!G H. G<=H ==> parts(G) <= parts(H)"; +Goalw parts.defs "G<=H ==> parts(G) <= parts(H)"; by (rtac lfp_mono 1); by (REPEAT (ares_tac basic_monos 1)); qed "parts_mono"; @@ -149,13 +149,13 @@ qed "parts_empty"; Addsimps [parts_empty]; -Goal "!!X. X: parts{} ==> P"; +Goal "X: parts{} ==> P"; by (Asm_full_simp_tac 1); qed "parts_emptyE"; AddSEs [parts_emptyE]; (*WARNING: loops if H = {Y}, therefore must not be repeated!*) -Goal "!!H. X: parts H ==> EX Y:H. X: parts {Y}"; +Goal "X: parts H ==> EX Y:H. X: parts {Y}"; by (etac parts.induct 1); by (ALLGOALS Blast_tac); qed "parts_singleton"; @@ -215,7 +215,7 @@ (** Idempotence and transitivity **) -Goal "!!H. X: parts (parts H) ==> X: parts H"; +Goal "X: parts (parts H) ==> X: parts H"; by (etac parts.induct 1); by (ALLGOALS Blast_tac); qed "parts_partsD"; @@ -226,19 +226,19 @@ qed "parts_idem"; Addsimps [parts_idem]; -Goal "!!H. [| X: parts G; G <= parts H |] ==> X: parts H"; +Goal "[| X: parts G; G <= parts H |] ==> X: parts H"; by (dtac parts_mono 1); by (Blast_tac 1); qed "parts_trans"; (*Cut*) -Goal "!!H. [| Y: parts (insert X G); X: parts H |] \ +Goal "[| Y: parts (insert X G); X: parts H |] \ \ ==> Y: parts (G Un H)"; by (etac parts_trans 1); by Auto_tac; qed "parts_cut"; -Goal "!!H. X: parts H ==> parts (insert X H) = parts H"; +Goal "X: parts H ==> parts (insert X H) = parts H"; by (fast_tac (claset() addSDs [parts_cut] addIs [parts_insertI] addss (simpset())) 1); @@ -366,7 +366,7 @@ Addsimps [analz_parts]; (*Monotonicity; Lemma 1 of Lowe*) -Goalw analz.defs "!!G H. G<=H ==> analz(G) <= analz(H)"; +Goalw analz.defs "G<=H ==> analz(G) <= analz(H)"; by (rtac lfp_mono 1); by (REPEAT (ares_tac basic_monos 1)); qed "analz_mono"; @@ -417,7 +417,7 @@ (*Can only pull out Keys if they are not needed to decrypt the rest*) Goalw [keysFor_def] - "!!K. K ~: keysFor (analz H) ==> \ + "K ~: keysFor (analz H) ==> \ \ analz (insert (Key K) H) = insert (Key K) (analz H)"; by (analz_tac 1); qed "analz_insert_Key"; @@ -433,13 +433,13 @@ qed "analz_insert_MPair"; (*Can pull out enCrypted message if the Key is not known*) -Goal "!!H. Key (invKey K) ~: analz H ==> \ +Goal "Key (invKey K) ~: analz H ==> \ \ analz (insert (Crypt K X) H) = \ \ insert (Crypt K X) (analz H)"; by (analz_tac 1); qed "analz_insert_Crypt"; -Goal "!!H. Key (invKey K) : analz H ==> \ +Goal "Key (invKey K) : analz H ==> \ \ analz (insert (Crypt K X) H) <= \ \ insert (Crypt K X) (analz (insert X H))"; by (rtac subsetI 1); @@ -447,7 +447,7 @@ by (ALLGOALS (Blast_tac)); val lemma1 = result(); -Goal "!!H. Key (invKey K) : analz H ==> \ +Goal "Key (invKey K) : analz H ==> \ \ insert (Crypt K X) (analz (insert X H)) <= \ \ analz (insert (Crypt K X) H)"; by Auto_tac; @@ -456,7 +456,7 @@ by (blast_tac (claset() addIs [analz_insertI, analz.Decrypt]) 1); val lemma2 = result(); -Goal "!!H. Key (invKey K) : analz H ==> \ +Goal "Key (invKey K) : analz H ==> \ \ analz (insert (Crypt K X) H) = \ \ insert (Crypt K X) (analz (insert X H))"; by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1)); @@ -499,7 +499,7 @@ (** Idempotence and transitivity **) -Goal "!!H. X: analz (analz H) ==> X: analz H"; +Goal "X: analz (analz H) ==> X: analz H"; by (etac analz.induct 1); by (ALLGOALS Blast_tac); qed "analz_analzD"; @@ -510,52 +510,52 @@ qed "analz_idem"; Addsimps [analz_idem]; -Goal "!!H. [| X: analz G; G <= analz H |] ==> X: analz H"; +Goal "[| X: analz G; G <= analz H |] ==> X: analz H"; by (dtac analz_mono 1); by (Blast_tac 1); qed "analz_trans"; (*Cut; Lemma 2 of Lowe*) -Goal "!!H. [| Y: analz (insert X H); X: analz H |] ==> Y: analz H"; +Goal "[| Y: analz (insert X H); X: analz H |] ==> Y: analz H"; by (etac analz_trans 1); by (Blast_tac 1); qed "analz_cut"; (*Cut can be proved easily by induction on - "!!H. Y: analz (insert X H) ==> X: analz H --> Y: analz H" + "Y: analz (insert X H) ==> X: analz H --> Y: analz H" *) (*This rewrite rule helps in the simplification of messages that involve the forwarding of unknown components (X). Without it, removing occurrences of X can be very complicated. *) -Goal "!!H. X: analz H ==> analz (insert X H) = analz H"; +Goal "X: analz H ==> analz (insert X H) = analz H"; by (blast_tac (claset() addIs [analz_cut, analz_insertI]) 1); qed "analz_insert_eq"; (** A congruence rule for "analz" **) -Goal "!!H. [| analz G <= analz G'; analz H <= analz H' \ +Goal "[| analz G <= analz G'; analz H <= analz H' \ \ |] ==> analz (G Un H) <= analz (G' Un H')"; by (Clarify_tac 1); by (etac analz.induct 1); by (ALLGOALS (best_tac (claset() addIs [analz_mono RS subsetD]))); qed "analz_subset_cong"; -Goal "!!H. [| analz G = analz G'; analz H = analz H' \ +Goal "[| analz G = analz G'; analz H = analz H' \ \ |] ==> analz (G Un H) = analz (G' Un H')"; by (REPEAT_FIRST (ares_tac [equalityI, analz_subset_cong] ORELSE' etac equalityE)); qed "analz_cong"; -Goal "!!H. analz H = analz H' ==> analz(insert X H) = analz(insert X H')"; +Goal "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"; by (asm_simp_tac (simpset() addsimps [insert_def] delsimps [singleton_conv] setloop (rtac analz_cong)) 1); qed "analz_insert_cong"; (*If there are no pairs or encryptions then analz does nothing*) -Goal "!!H. [| ALL X Y. {|X,Y|} ~: H; ALL X K. Crypt K X ~: H |] ==> \ +Goal "[| ALL X Y. {|X,Y|} ~: H; ALL X K. Crypt K X ~: H |] ==> \ \ analz H = H"; by Safe_tac; by (etac analz.induct 1); @@ -563,7 +563,7 @@ qed "analz_trivial"; (*These two are obsolete (with a single Spy) but cost little to prove...*) -Goal "!!X. X: analz (UN i:A. analz (H i)) ==> X: analz (UN i:A. H i)"; +Goal "X: analz (UN i:A. analz (H i)) ==> X: analz (UN i:A. H i)"; by (etac analz.induct 1); by (ALLGOALS (blast_tac (claset() addIs [impOfSubs analz_mono]))); val lemma = result(); @@ -596,7 +596,7 @@ qed "synth_increasing"; (*Monotonicity*) -Goalw synth.defs "!!G H. G<=H ==> synth(G) <= synth(H)"; +Goalw synth.defs "G<=H ==> synth(G) <= synth(H)"; by (rtac lfp_mono 1); by (REPEAT (ares_tac basic_monos 1)); qed "synth_mono"; @@ -615,7 +615,7 @@ (** Idempotence and transitivity **) -Goal "!!H. X: synth (synth H) ==> X: synth H"; +Goal "X: synth (synth H) ==> X: synth H"; by (etac synth.induct 1); by (ALLGOALS Blast_tac); qed "synth_synthD"; @@ -625,13 +625,13 @@ by (Blast_tac 1); qed "synth_idem"; -Goal "!!H. [| X: synth G; G <= synth H |] ==> X: synth H"; +Goal "[| X: synth G; G <= synth H |] ==> X: synth H"; by (dtac synth_mono 1); by (Blast_tac 1); qed "synth_trans"; (*Cut; Lemma 2 of Lowe*) -Goal "!!H. [| Y: synth (insert X H); X: synth H |] ==> Y: synth H"; +Goal "[| Y: synth (insert X H); X: synth H |] ==> Y: synth H"; by (etac synth_trans 1); by (Blast_tac 1); qed "synth_cut"; @@ -652,7 +652,7 @@ by (Blast_tac 1); qed "Key_synth_eq"; -Goal "!!K. Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X : H)"; +Goal "Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X : H)"; by (Blast_tac 1); qed "Crypt_synth_eq"; @@ -701,23 +701,23 @@ (** For reasoning about the Fake rule in traces **) -Goal "!!Y. X: G ==> parts(insert X H) <= parts G Un parts H"; +Goal "X: G ==> parts(insert X H) <= parts G Un parts H"; by (rtac ([parts_mono, parts_Un_subset2] MRS subset_trans) 1); by (Blast_tac 1); qed "parts_insert_subset_Un"; (*More specifically for Fake. Very occasionally we could do with a version of the form parts{X} <= synth (analz H) Un parts H *) -Goal "!!H. X: synth (analz H) ==> \ -\ parts (insert X H) <= synth (analz H) Un parts H"; +Goal "X: synth (analz H) ==> \ +\ parts (insert X H) <= synth (analz H) Un parts H"; by (dtac parts_insert_subset_Un 1); by (Full_simp_tac 1); by (Blast_tac 1); qed "Fake_parts_insert"; (*H is sometimes (Key `` KK Un spies evs), so can't put G=H*) -Goal "!!H. X: synth (analz G) ==> \ -\ analz (insert X H) <= synth (analz G) Un analz (G Un H)"; +Goal "X: synth (analz G) ==> \ +\ analz (insert X H) <= synth (analz G) Un analz (G Un H)"; by (rtac subsetI 1); by (subgoal_tac "x : analz (synth (analz G) Un H)" 1); by (blast_tac (claset() addIs [impOfSubs analz_mono, @@ -739,20 +739,20 @@ (*Without this equation, other rules for synth and analz would yield redundant cases*) Goal "({|X,Y|} : synth (analz H)) = \ -\ (X : synth (analz H) & Y : synth (analz H))"; +\ (X : synth (analz H) & Y : synth (analz H))"; by (Blast_tac 1); qed "MPair_synth_analz"; AddIffs [MPair_synth_analz]; -Goal "!!K. [| Key K : analz H; Key (invKey K) : analz H |] \ -\ ==> (Crypt K X : synth (analz H)) = (X : synth (analz H))"; +Goal "[| Key K : analz H; Key (invKey K) : analz H |] \ +\ ==> (Crypt K X : synth (analz H)) = (X : synth (analz H))"; by (Blast_tac 1); qed "Crypt_synth_analz"; -Goal "!!K. X ~: synth (analz H) \ -\ ==> (Hash{|X,Y|} : synth (analz H)) = (Hash{|X,Y|} : analz H)"; +Goal "X ~: synth (analz H) \ +\ ==> (Hash{|X,Y|} : synth (analz H)) = (Hash{|X,Y|} : analz H)"; by (Blast_tac 1); qed "Hash_synth_analz"; Addsimps [Hash_synth_analz]; @@ -825,7 +825,7 @@ by (Simp_tac 1); qed "analz_insert_HPair"; -Goalw [HPair_def] "!!H. X ~: synth (analz H) \ +Goalw [HPair_def] "X ~: synth (analz H) \ \ ==> (Hash[X] Y : synth (analz H)) = \ \ (Hash {|X, Y|} : analz H & Y : synth (analz H))"; by (Simp_tac 1); diff -r c4da11bb0592 -r c729d4c299c1 src/HOL/Auth/NS_Public.ML --- a/src/HOL/Auth/NS_Public.ML Thu Jul 02 17:27:35 1998 +0200 +++ b/src/HOL/Auth/NS_Public.ML Thu Jul 02 17:48:11 1998 +0200 @@ -19,9 +19,8 @@ AddIffs [Spy_in_bad]; (*A "possibility property": there are traces that reach the end*) -Goal - "!!A B. A ~= B ==> EX NB. EX evs: ns_public. \ -\ Says A B (Crypt (pubK B) (Nonce NB)) : set evs"; +Goal "A ~= B ==> EX NB. EX evs: ns_public. \ +\ Says A B (Crypt (pubK B) (Nonce NB)) : set evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2); by possibility_tac; @@ -31,7 +30,7 @@ (**** Inductive proofs about ns_public ****) (*Nobody sends themselves messages*) -Goal "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set evs"; +Goal "evs : ns_public ==> ALL A X. Says A A X ~: set evs"; by (etac ns_public.induct 1); by Auto_tac; qed_spec_mp "not_Says_to_self"; @@ -54,15 +53,13 @@ sends messages containing X! **) (*Spy never sees another agent's private key! (unless it's bad at start)*) -Goal - "!!A. evs: ns_public ==> (Key (priK A) : parts (spies evs)) = (A : bad)"; +Goal "evs: ns_public ==> (Key (priK A) : parts (spies evs)) = (A : bad)"; by (parts_induct_tac 1); by (Blast_tac 1); qed "Spy_see_priK"; Addsimps [Spy_see_priK]; -Goal - "!!A. evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)"; +Goal "evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)"; by Auto_tac; qed "Spy_analz_priK"; Addsimps [Spy_analz_priK]; @@ -75,9 +72,8 @@ (*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce is secret. (Honest users generate fresh nonces.)*) -Goal - "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \ -\ Nonce NA ~: analz (spies evs); evs : ns_public |] \ +Goal "[| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \ +\ Nonce NA ~: analz (spies evs); evs : ns_public |] \ \ ==> Crypt (pubK C) {|NA', Nonce NA, Agent D|} ~: parts (spies evs)"; by (etac rev_mp 1); by (etac rev_mp 1); @@ -90,11 +86,10 @@ (*Unicity for NS1: nonce NA identifies agents A and B*) -Goal - "!!evs. [| Nonce NA ~: analz (spies evs); evs : ns_public |] \ +Goal "[| Nonce NA ~: analz (spies evs); evs : ns_public |] \ \ ==> EX A' B'. ALL A B. \ -\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \ -\ A=A' & B=B'"; +\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \ +\ A=A' & B=B'"; by (etac rev_mp 1); by (parts_induct_tac 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); @@ -105,12 +100,11 @@ by (Blast_tac 1); val lemma = result(); -Goal - "!!evs. [| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(spies evs); \ -\ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies evs); \ -\ Nonce NA ~: analz (spies evs); \ -\ evs : ns_public |] \ -\ ==> A=A' & B=B'"; +Goal "[| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(spies evs); \ +\ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies evs); \ +\ Nonce NA ~: analz (spies evs); \ +\ evs : ns_public |] \ +\ ==> A=A' & B=B'"; by (prove_unique_tac lemma 1); qed "unique_NA"; @@ -122,10 +116,9 @@ (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*) -Goal - "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \ -\ A ~: bad; B ~: bad; evs : ns_public |] \ -\ ==> Nonce NA ~: analz (spies evs)"; +Goal "[| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \ +\ A ~: bad; B ~: bad; evs : ns_public |] \ +\ ==> Nonce NA ~: analz (spies evs)"; by (etac rev_mp 1); by (analz_induct_tac 1); (*NS3*) @@ -141,13 +134,12 @@ (*Authentication for A: if she receives message 2 and has used NA to start a run, then B has sent message 2.*) -Goal - "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \ -\ Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ -\ : set evs; \ -\ A ~: bad; B ~: bad; evs : ns_public |] \ -\ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ -\ : set evs"; +Goal "[| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \ +\ Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ +\ : set evs; \ +\ A ~: bad; B ~: bad; evs : ns_public |] \ +\ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ +\ : set evs"; by (etac rev_mp 1); (*prepare induction over Crypt (pubK A) {|NA,NB,B|} : parts H*) by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1); @@ -161,11 +153,10 @@ (*If the encrypted message appears then it originated with Alice in NS1*) -Goal - "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \ -\ Nonce NA ~: analz (spies evs); \ -\ evs : ns_public |] \ -\ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs"; +Goal "[| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \ +\ Nonce NA ~: analz (spies evs); \ +\ evs : ns_public |] \ +\==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs"; by (etac rev_mp 1); by (etac rev_mp 1); by (parts_induct_tac 1); @@ -179,11 +170,10 @@ (*Unicity for NS2: nonce NB identifies nonce NA and agents A, B [unicity of B makes Lowe's fix work] [proof closely follows that for unique_NA] *) -Goal - "!!evs. [| Nonce NB ~: analz (spies evs); evs : ns_public |] \ +Goal "[| Nonce NB ~: analz (spies evs); evs : ns_public |] \ \ ==> EX A' NA' B'. ALL A NA B. \ -\ Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|} : parts (spies evs) \ -\ --> A=A' & NA=NA' & B=B'"; +\ Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|} : parts (spies evs) \ +\ --> A=A' & NA=NA' & B=B'"; by (etac rev_mp 1); by (parts_induct_tac 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); @@ -194,14 +184,13 @@ by (Blast_tac 1); val lemma = result(); -Goal - "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|} \ -\ : parts(spies evs); \ -\ Crypt(pubK A') {|Nonce NA', Nonce NB, Agent B'|} \ -\ : parts(spies evs); \ -\ Nonce NB ~: analz (spies evs); \ -\ evs : ns_public |] \ -\ ==> A=A' & NA=NA' & B=B'"; +Goal "[| Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|} \ +\ : parts(spies evs); \ +\ Crypt(pubK A') {|Nonce NA', Nonce NB, Agent B'|} \ +\ : parts(spies evs); \ +\ Nonce NB ~: analz (spies evs); \ +\ evs : ns_public |] \ +\ ==> A=A' & NA=NA' & B=B'"; by (prove_unique_tac lemma 1); qed "unique_NB"; @@ -209,10 +198,9 @@ (*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*) -Goal - "!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ -\ : set evs; \ -\ A ~: bad; B ~: bad; evs : ns_public |] \ +Goal "[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ +\ : set evs; \ +\ A ~: bad; B ~: bad; evs : ns_public |] \ \ ==> Nonce NB ~: analz (spies evs)"; by (etac rev_mp 1); by (analz_induct_tac 1); @@ -231,12 +219,11 @@ (*Authentication for B: if he receives message 3 and has used NB in message 2, then A has sent message 3.*) -Goal - "!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ -\ : set evs; \ -\ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \ -\ A ~: bad; B ~: bad; evs : ns_public |] \ -\ ==> Says A B (Crypt (pubK B) (Nonce NB)) : set evs"; +Goal "[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ +\ : set evs; \ +\ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \ +\ A ~: bad; B ~: bad; evs : ns_public |] \ +\ ==> Says A B (Crypt (pubK B) (Nonce NB)) : set evs"; by (etac rev_mp 1); (*prepare induction over Crypt (pubK B) NB : parts H*) by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1); @@ -255,12 +242,11 @@ (*If B receives NS3 and the nonce NB agrees with the nonce he joined with NA, then A initiated the run using NA. SAME proof as B_trusts_NS3!*) -Goal - "!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ -\ : set evs; \ -\ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \ -\ A ~: bad; B ~: bad; evs : ns_public |] \ -\ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs"; +Goal "[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ +\ : set evs; \ +\ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \ +\ A ~: bad; B ~: bad; evs : ns_public |] \ +\ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs"; by (etac rev_mp 1); (*prepare induction over Crypt (pubK B) {|NB|} : parts H*) by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1); diff -r c4da11bb0592 -r c729d4c299c1 src/HOL/Auth/NS_Public_Bad.ML --- a/src/HOL/Auth/NS_Public_Bad.ML Thu Jul 02 17:27:35 1998 +0200 +++ b/src/HOL/Auth/NS_Public_Bad.ML Thu Jul 02 17:48:11 1998 +0200 @@ -23,9 +23,8 @@ AddIffs [Spy_in_bad]; (*A "possibility property": there are traces that reach the end*) -Goal - "!!A B. A ~= B ==> EX NB. EX evs: ns_public. \ -\ Says A B (Crypt (pubK B) (Nonce NB)) : set evs"; +Goal "A ~= B ==> EX NB. EX evs: ns_public. \ +\ Says A B (Crypt (pubK B) (Nonce NB)) : set evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2); by possibility_tac; @@ -35,7 +34,7 @@ (**** Inductive proofs about ns_public ****) (*Nobody sends themselves messages*) -Goal "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set evs"; +Goal "evs : ns_public ==> ALL A X. Says A A X ~: set evs"; by (etac ns_public.induct 1); by Auto_tac; qed_spec_mp "not_Says_to_self"; @@ -58,15 +57,13 @@ sends messages containing X! **) (*Spy never sees another agent's private key! (unless it's bad at start)*) -Goal - "!!A. evs: ns_public ==> (Key (priK A) : parts (spies evs)) = (A : bad)"; +Goal "evs: ns_public ==> (Key (priK A) : parts (spies evs)) = (A : bad)"; by (parts_induct_tac 1); by (Blast_tac 1); qed "Spy_see_priK"; Addsimps [Spy_see_priK]; -Goal - "!!A. evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)"; +Goal "evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)"; by Auto_tac; qed "Spy_analz_priK"; Addsimps [Spy_analz_priK]; @@ -79,9 +76,8 @@ (*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce is secret. (Honest users generate fresh nonces.)*) -Goal - "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \ -\ Nonce NA ~: analz (spies evs); evs : ns_public |] \ +Goal "[| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \ +\ Nonce NA ~: analz (spies evs); evs : ns_public |] \ \ ==> Crypt (pubK C) {|NA', Nonce NA|} ~: parts (spies evs)"; by (etac rev_mp 1); by (etac rev_mp 1); @@ -94,11 +90,10 @@ (*Unicity for NS1: nonce NA identifies agents A and B*) -Goal - "!!evs. [| Nonce NA ~: analz (spies evs); evs : ns_public |] \ +Goal "[| Nonce NA ~: analz (spies evs); evs : ns_public |] \ \ ==> EX A' B'. ALL A B. \ -\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \ -\ A=A' & B=B'"; +\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \ +\ A=A' & B=B'"; by (etac rev_mp 1); by (parts_induct_tac 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); @@ -109,12 +104,11 @@ by (Blast_tac 1); val lemma = result(); -Goal - "!!evs. [| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(spies evs); \ -\ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies evs); \ -\ Nonce NA ~: analz (spies evs); \ -\ evs : ns_public |] \ -\ ==> A=A' & B=B'"; +Goal "[| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(spies evs); \ +\ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies evs); \ +\ Nonce NA ~: analz (spies evs); \ +\ evs : ns_public |] \ +\ ==> A=A' & B=B'"; by (prove_unique_tac lemma 1); qed "unique_NA"; @@ -126,10 +120,9 @@ (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*) -Goal - "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \ -\ A ~: bad; B ~: bad; evs : ns_public |] \ -\ ==> Nonce NA ~: analz (spies evs)"; +Goal "[| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \ +\ A ~: bad; B ~: bad; evs : ns_public |] \ +\ ==> Nonce NA ~: analz (spies evs)"; by (etac rev_mp 1); by (analz_induct_tac 1); (*NS3*) @@ -145,11 +138,10 @@ (*Authentication for A: if she receives message 2 and has used NA to start a run, then B has sent message 2.*) -Goal - "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \ -\ Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs; \ -\ A ~: bad; B ~: bad; evs : ns_public |] \ -\ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs"; +Goal "[| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \ +\ Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs; \ +\ A ~: bad; B ~: bad; evs : ns_public |] \ +\ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs"; by (etac rev_mp 1); (*prepare induction over Crypt (pubK A) {|NA,NB|} : parts H*) by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1); @@ -166,11 +158,10 @@ (*If the encrypted message appears then it originated with Alice in NS1*) -Goal - "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \ -\ Nonce NA ~: analz (spies evs); \ -\ evs : ns_public |] \ -\ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs"; +Goal "[| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \ +\ Nonce NA ~: analz (spies evs); \ +\ evs : ns_public |] \ +\==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs"; by (etac rev_mp 1); by (etac rev_mp 1); by (parts_induct_tac 1); @@ -183,11 +174,10 @@ (*Unicity for NS2: nonce NB identifies nonce NA and agent A [proof closely follows that for unique_NA] *) -Goal - "!!evs. [| Nonce NB ~: analz (spies evs); evs : ns_public |] \ +Goal "[| Nonce NB ~: analz (spies evs); evs : ns_public |] \ \ ==> EX A' NA'. ALL A NA. \ -\ Crypt (pubK A) {|Nonce NA, Nonce NB|} : parts (spies evs) \ -\ --> A=A' & NA=NA'"; +\ Crypt (pubK A) {|Nonce NA, Nonce NB|} : parts (spies evs) \ +\ --> A=A' & NA=NA'"; by (etac rev_mp 1); by (parts_induct_tac 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); @@ -197,22 +187,20 @@ by (Blast_tac 1); val lemma = result(); -Goal - "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB|} : parts(spies evs); \ -\ Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(spies evs); \ -\ Nonce NB ~: analz (spies evs); \ -\ evs : ns_public |] \ -\ ==> A=A' & NA=NA'"; +Goal "[| Crypt(pubK A) {|Nonce NA, Nonce NB|} : parts(spies evs); \ +\ Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(spies evs); \ +\ Nonce NB ~: analz (spies evs); \ +\ evs : ns_public |] \ +\ ==> A=A' & NA=NA'"; by (prove_unique_tac lemma 1); qed "unique_NB"; (*NB remains secret PROVIDED Alice never responds with round 3*) -Goal - "!!evs.[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs; \ -\ ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set evs; \ -\ A ~: bad; B ~: bad; evs : ns_public |] \ -\ ==> Nonce NB ~: analz (spies evs)"; +Goal "[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs; \ +\ ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set evs; \ +\ A ~: bad; B ~: bad; evs : ns_public |] \ +\ ==> Nonce NB ~: analz (spies evs)"; by (etac rev_mp 1); by (etac rev_mp 1); by (analz_induct_tac 1); @@ -232,11 +220,10 @@ (*Authentication for B: if he receives message 3 and has used NB in message 2, then A has sent message 3--to somebody....*) -Goal - "!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs; \ -\ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \ -\ A ~: bad; B ~: bad; evs : ns_public |] \ -\ ==> EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set evs"; +Goal "[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs; \ +\ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \ +\ A ~: bad; B ~: bad; evs : ns_public |] \ +\ ==> EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set evs"; by (etac rev_mp 1); (*prepare induction over Crypt (pubK B) NB : parts H*) by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1); @@ -254,10 +241,9 @@ (*Can we strengthen the secrecy theorem? NO*) -Goal - "!!evs. [| A ~: bad; B ~: bad; evs : ns_public |] \ +Goal "[| A ~: bad; B ~: bad; evs : ns_public |] \ \ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs \ -\ --> Nonce NB ~: analz (spies evs)"; +\ --> Nonce NB ~: analz (spies evs)"; by (analz_induct_tac 1); by (ALLGOALS Clarify_tac); (*NS2: by freshness and unicity of NB*) diff -r c4da11bb0592 -r c729d4c299c1 src/HOL/Auth/NS_Shared.ML --- a/src/HOL/Auth/NS_Shared.ML Thu Jul 02 17:27:35 1998 +0200 +++ b/src/HOL/Auth/NS_Shared.ML Thu Jul 02 17:48:11 1998 +0200 @@ -22,7 +22,7 @@ (*A "possibility property": there are traces that reach the end*) Goal - "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ + "[| A ~= B; A ~= Server; B ~= Server |] \ \ ==> EX N K. EX evs: ns_shared. \ \ Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); @@ -32,7 +32,7 @@ result(); Goal - "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ + "[| A ~= B; A ~= Server; B ~= Server |] \ \ ==> EX evs: ns_shared. \ \ Says A B (Crypt ?K {|Nonce ?N, Nonce ?N|}) : set evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); @@ -43,7 +43,7 @@ (**** Inductive proofs about ns_shared ****) (*Nobody sends themselves messages*) -Goal "!!evs. evs : ns_shared ==> ALL A X. Says A A X ~: set evs"; +Goal "evs : ns_shared ==> ALL A X. Says A A X ~: set evs"; by (etac ns_shared.induct 1); by Auto_tac; qed_spec_mp "not_Says_to_self"; @@ -51,13 +51,13 @@ AddSEs [not_Says_to_self RSN (2, rev_notE)]; (*For reasoning about the encrypted portion of message NS3*) -Goal "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set evs \ +Goal "Says S A (Crypt KA {|N, B, K, X|}) : set evs \ \ ==> X : parts (spies evs)"; by (Blast_tac 1); qed "NS3_msg_in_parts_spies"; Goal - "!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set evs \ + "Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set evs \ \ ==> K : parts (spies evs)"; by (Blast_tac 1); qed "Oops_parts_spies"; @@ -76,14 +76,14 @@ (*Spy never sees another agent's shared key! (unless it's bad at start)*) Goal - "!!evs. evs : ns_shared ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; + "evs : ns_shared ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; by (parts_induct_tac 1); by (ALLGOALS Blast_tac); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; Goal - "!!evs. evs : ns_shared ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; + "evs : ns_shared ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; by Auto_tac; qed "Spy_analz_shrK"; Addsimps [Spy_analz_shrK]; @@ -93,7 +93,7 @@ (*Nobody can have used non-existent keys!*) -Goal "!!evs. evs : ns_shared ==> \ +Goal "evs : ns_shared ==> \ \ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; by (parts_induct_tac 1); (*Fake*) @@ -113,7 +113,7 @@ (*Describes the form of K, X and K' when the Server sends this message.*) Goal - "!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) : set evs; \ + "[| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) : set evs; \ \ evs : ns_shared |] \ \ ==> K ~: range shrK & \ \ X = (Crypt (shrK B) {|Key K, Agent A|}) & \ @@ -126,7 +126,7 @@ (*If the encrypted message appears then it originated with the Server*) Goal - "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \ + "[| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \ \ A ~: bad; evs : ns_shared |] \ \ ==> Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \ \ : set evs"; @@ -137,7 +137,7 @@ Goal - "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \ + "[| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \ \ A ~: bad; evs : ns_shared |] \ \ ==> K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|})"; by (blast_tac (claset() addSDs [A_trusts_NS2, Says_Server_message_form]) 1); @@ -148,7 +148,7 @@ OR reduces it to the Fake case. Use Says_Server_message_form if applicable.*) Goal - "!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) \ + "[| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) \ \ : set evs; \ \ evs : ns_shared |] \ \ ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|})) \ @@ -181,7 +181,7 @@ to encrypt messages containing other keys, in the actual protocol. We require that agents should behave like this subsequently also.*) Goal - "!!evs. [| evs : ns_shared; Kab ~: range shrK |] ==> \ + "[| evs : ns_shared; Kab ~: range shrK |] ==> \ \ (Crypt KAB X) : parts (spies evs) & \ \ Key K : parts {X} --> Key K : parts (spies evs)"; by (parts_induct_tac 1); @@ -197,7 +197,7 @@ (*The equality makes the induction hypothesis easier to apply*) Goal - "!!evs. evs : ns_shared ==> \ + "evs : ns_shared ==> \ \ ALL K KK. KK <= Compl (range shrK) --> \ \ (Key K : analz (Key``KK Un (spies evs))) = \ \ (K : KK | Key K : analz (spies evs))"; @@ -213,7 +213,7 @@ Goal - "!!evs. [| evs : ns_shared; KAB ~: range shrK |] ==> \ + "[| evs : ns_shared; 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); @@ -223,7 +223,7 @@ (** The session key K uniquely identifies the message **) Goal - "!!evs. evs : ns_shared ==> \ + "evs : ns_shared ==> \ \ EX A' NA' B' X'. ALL A NA B X. \ \ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs \ \ --> A=A' & NA=NA' & B=B' & X=X'"; @@ -241,7 +241,7 @@ (*In messages of this form, the session key uniquely identifies the rest*) Goal - "!!evs. [| Says Server A \ + "[| Says Server A \ \ (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs; \ \ Says Server A' \ \ (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) : set evs; \ @@ -253,7 +253,7 @@ (** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **) Goal - "!!evs. [| A ~: bad; B ~: bad; evs : ns_shared |] \ + "[| A ~: bad; B ~: bad; evs : ns_shared |] \ \ ==> Says Server A \ \ (Crypt (shrK A) {|NA, Agent B, Key K, \ \ Crypt (shrK B) {|Key K, Agent A|}|}) \ @@ -286,7 +286,7 @@ (*Final version: Server's message in the most abstract form*) Goal - "!!evs. [| Says Server A \ + "[| Says Server A \ \ (Crypt K' {|NA, Agent B, Key K, X|}) : set evs; \ \ ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \ \ A ~: bad; B ~: bad; evs : ns_shared \ @@ -303,7 +303,7 @@ (*If the encrypted message appears then it originated with the Server*) Goal - "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs); \ + "[| Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs); \ \ B ~: bad; evs : ns_shared |] \ \ ==> EX NA. Says Server A \ \ (Crypt (shrK A) {|NA, Agent B, Key K, \ @@ -316,7 +316,7 @@ Goal - "!!evs. [| Crypt K (Nonce NB) : parts (spies evs); \ + "[| Crypt K (Nonce NB) : parts (spies evs); \ \ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \ \ : set evs; \ \ Key K ~: analz (spies evs); \ @@ -343,7 +343,7 @@ (*This version no longer assumes that K is secure*) Goal - "!!evs. [| Crypt K (Nonce NB) : parts (spies evs); \ + "[| Crypt K (Nonce NB) : parts (spies evs); \ \ Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \ \ ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \ \ A ~: bad; B ~: bad; evs : ns_shared |] \ @@ -357,7 +357,7 @@ component X in some instance of NS4. Perhaps an interesting property, but not needed (after all) for the proofs below.*) Goal - "!!evs. [| Crypt K (Nonce NB) : parts (spies evs); \ + "[| Crypt K (Nonce NB) : parts (spies evs); \ \ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \ \ : set evs; \ \ Key K ~: analz (spies evs); \ @@ -384,7 +384,7 @@ Goal - "!!evs. [| B ~: bad; evs : ns_shared |] \ + "[| B ~: bad; evs : ns_shared |] \ \ ==> Key K ~: analz (spies evs) --> \ \ Says Server A \ \ (Crypt (shrK A) {|NA, Agent B, Key K, \ @@ -412,7 +412,7 @@ (*Very strong Oops condition reveals protocol's weakness*) Goal - "!!evs. [| Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs); \ + "[| Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs); \ \ Says B A (Crypt K (Nonce NB)) : set evs; \ \ Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs); \ \ ALL NA NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \ diff -r c4da11bb0592 -r c729d4c299c1 src/HOL/Auth/OtwayRees.ML --- a/src/HOL/Auth/OtwayRees.ML Thu Jul 02 17:27:35 1998 +0200 +++ b/src/HOL/Auth/OtwayRees.ML Thu Jul 02 17:48:11 1998 +0200 @@ -24,10 +24,10 @@ (*A "possibility property": there are traces that reach the end*) Goal - "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ -\ ==> EX K. EX NA. EX evs: otway. \ -\ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \ -\ : set evs"; + "[| A ~= B; A ~= Server; B ~= Server |] \ +\ ==> EX K. EX NA. EX evs: otway. \ +\ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \ +\ : set evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2); by possibility_tac; @@ -37,7 +37,7 @@ (**** Inductive proofs about otway ****) (*Nobody sends themselves messages*) -Goal "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs"; +Goal "evs : otway ==> ALL A X. Says A A X ~: set evs"; by (etac otway.induct 1); by Auto_tac; qed_spec_mp "not_Says_to_self"; @@ -47,20 +47,20 @@ (** For reasoning about the encrypted portion of messages **) -Goal "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \ -\ ==> X : analz (spies evs)"; +Goal "Says A' B {|N, Agent A, Agent B, X|} : set evs \ +\ ==> X : analz (spies evs)"; by (dtac (Says_imp_spies RS analz.Inj) 1); by (Blast_tac 1); qed "OR2_analz_spies"; -Goal "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \ -\ ==> X : analz (spies evs)"; +Goal "Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \ +\ ==> X : analz (spies evs)"; by (dtac (Says_imp_spies RS analz.Inj) 1); by (Blast_tac 1); qed "OR4_analz_spies"; -Goal "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \ -\ ==> K : parts (spies evs)"; +Goal "Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \ +\ ==> K : parts (spies evs)"; by (Blast_tac 1); qed "Oops_parts_spies"; @@ -83,14 +83,14 @@ (*Spy never sees a good agent's shared key!*) Goal - "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; + "evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; by (parts_induct_tac 1); by (ALLGOALS Blast_tac); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; Goal - "!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; + "evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); qed "Spy_analz_shrK"; Addsimps [Spy_analz_shrK]; @@ -100,8 +100,8 @@ (*Nobody can have used non-existent keys!*) -Goal "!!evs. 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); @@ -122,8 +122,8 @@ (*Describes the form of K and NA when the Server sends this message. Also for Oops case.*) Goal - "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \ -\ evs : otway |] \ + "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \ +\ 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); @@ -154,10 +154,10 @@ (*The equality makes the induction hypothesis easier to apply*) Goal - "!!evs. evs : otway ==> \ + "evs : otway ==> \ \ ALL K KK. KK <= Compl (range shrK) --> \ -\ (Key K : analz (Key``KK Un (spies evs))) = \ -\ (K : KK | Key K : analz (spies evs))"; +\ (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])); @@ -169,9 +169,9 @@ Goal - "!!evs. [| evs : otway; KAB ~: range shrK |] ==> \ -\ Key K : analz (insert (Key KAB) (spies evs)) = \ -\ (K = KAB | Key K : analz (spies evs))"; + "[| 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"; @@ -179,7 +179,7 @@ (*** The Key K uniquely identifies the Server's message. **) Goal - "!!evs. evs : otway ==> \ + "evs : otway ==> \ \ 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'"; @@ -196,9 +196,9 @@ val lemma = result(); Goal - "!!evs. [| 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'"; + "[| 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 (prove_unique_tac lemma 1); qed "unique_session_keys"; @@ -208,11 +208,11 @@ (*Only OR1 can have caused such a part of a message to appear.*) Goal - "!!evs. [| A ~: bad; evs : otway |] \ -\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \ -\ Says A 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|} : parts (spies evs) --> \ +\ Says A B {|NA, Agent A, Agent B, \ +\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ +\ : set evs"; by (parts_induct_tac 1); by (Blast_tac 1); qed_spec_mp "Crypt_imp_OR1"; @@ -221,7 +221,7 @@ (** The Nonce NA uniquely identifies A's message. **) Goal - "!!evs. [| evs : otway; A ~: bad |] \ + "[| evs : otway; A ~: bad |] \ \ ==> EX B'. ALL B. \ \ Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) \ \ --> B = B'"; @@ -234,7 +234,7 @@ val lemma = result(); Goal - "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (spies evs); \ + "[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (spies evs); \ \ Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (spies evs); \ \ evs : otway; A ~: bad |] \ \ ==> B = C"; @@ -246,7 +246,7 @@ OR2 encrypts Nonce NB. It prevents the attack that can occur in the over-simplified version of this protocol: see OtwayRees_Bad.*) Goal - "!!evs. [| A ~: bad; evs : otway |] \ + "[| A ~: bad; evs : otway |] \ \ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \ \ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \ \ ~: parts (spies evs)"; @@ -259,7 +259,7 @@ (*Crucial property: If the encrypted message appears, and A has used NA to start a run, then it originated with the Server!*) Goal - "!!evs. [| A ~: bad; evs : otway |] \ + "[| A ~: bad; evs : otway |] \ \ ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs) \ \ --> Says A B {|NA, Agent A, Agent B, \ \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ @@ -291,15 +291,15 @@ bad form of this protocol, even though we can prove Spy_not_see_encrypted_key*) Goal - "!!evs. [| Says A B {|NA, Agent A, Agent B, \ -\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \ -\ Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \ -\ A ~: bad; evs : otway |] \ -\ ==> EX NB. Says Server B \ -\ {|NA, \ -\ Crypt (shrK A) {|NA, Key K|}, \ -\ Crypt (shrK B) {|NB, Key K|}|} \ -\ : set evs"; + "[| Says A B {|NA, Agent A, Agent B, \ +\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \ +\ Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \ +\ A ~: bad; evs : otway |] \ +\ ==> EX NB. Says Server B \ +\ {|NA, \ +\ Crypt (shrK A) {|NA, Key K|}, \ +\ Crypt (shrK B) {|NB, Key K|}|} \ +\ : set evs"; by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1); qed "A_trusts_OR4"; @@ -309,12 +309,12 @@ the premises, e.g. by having A=Spy **) Goal - "!!evs. [| A ~: bad; B ~: bad; evs : otway |] \ -\ ==> Says Server B \ -\ {|NA, Crypt (shrK A) {|NA, Key K|}, \ -\ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \ -\ Notes Spy {|NA, NB, Key K|} ~: set evs --> \ -\ Key K ~: analz (spies evs)"; + "[| A ~: bad; B ~: bad; evs : otway |] \ +\ ==> Says Server B \ +\ {|NA, Crypt (shrK A) {|NA, Key K|}, \ +\ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \ +\ Notes Spy {|NA, NB, Key K|} ~: set evs --> \ +\ Key K ~: analz (spies evs)"; by (etac otway.induct 1); by analz_spies_tac; by (ALLGOALS @@ -331,13 +331,12 @@ by (spy_analz_tac 1); val lemma = result() RS mp RS mp RSN(2,rev_notE); -Goal - "!!evs. [| Says Server B \ -\ {|NA, Crypt (shrK A) {|NA, Key K|}, \ -\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \ -\ Notes Spy {|NA, NB, Key K|} ~: set evs; \ -\ A ~: bad; B ~: bad; evs : otway |] \ -\ ==> Key K ~: analz (spies evs)"; +Goal "[| Says Server B \ +\ {|NA, Crypt (shrK A) {|NA, Key K|}, \ +\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \ +\ Notes Spy {|NA, NB, Key K|} ~: set evs; \ +\ A ~: bad; B ~: bad; evs : otway |] \ +\ ==> Key K ~: analz (spies 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"; @@ -345,13 +344,12 @@ (*A's guarantee. The Oops premise quantifies over NB because A cannot know what it is.*) -Goal - "!!evs. [| Says A B {|NA, Agent A, Agent B, \ -\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \ -\ Says B' 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 |] \ -\ ==> Key K ~: analz (spies evs)"; +Goal "[| Says A B {|NA, Agent A, Agent B, \ +\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \ +\ Says B' 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 |] \ +\ ==> Key K ~: analz (spies evs)"; by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1); qed "A_gets_good_key"; @@ -361,13 +359,13 @@ (*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 - "!!evs. [| B ~: bad; evs : otway |] \ -\ ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \ -\ : parts (spies evs) --> \ -\ (EX X. Says B Server \ -\ {|NA, Agent A, Agent B, X, \ -\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ -\ : set evs)"; + "[| B ~: bad; evs : otway |] \ +\ ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \ +\ : parts (spies evs) --> \ +\ (EX X. Says B Server \ +\ {|NA, Agent A, Agent B, X, \ +\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ +\ : set evs)"; by (parts_induct_tac 1); by (ALLGOALS Blast_tac); bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE); @@ -375,8 +373,7 @@ (** The Nonce NB uniquely identifies B's message. **) -Goal - "!!evs. [| evs : otway; B ~: bad |] \ +Goal "[| evs : otway; B ~: bad |] \ \ ==> EX NA' A'. ALL NA A. \ \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs) \ \ --> NA = NA' & A = A'"; @@ -389,7 +386,7 @@ val lemma = result(); Goal - "!!evs.[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs); \ + "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs); \ \ Crypt (shrK B) {|NC, NB, Agent C, Agent B|} : parts(spies evs); \ \ evs : otway; B ~: bad |] \ \ ==> NC = NA & C = A"; @@ -399,16 +396,15 @@ (*If the encrypted message appears, and B has used Nonce NB, then it originated with the Server!*) -Goal - "!!evs. [| B ~: bad; evs : otway |] \ -\ ==> Crypt (shrK B) {|NB, Key K|} : parts (spies evs) \ -\ --> (ALL X'. Says B Server \ -\ {|NA, Agent A, Agent B, X', \ -\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ -\ : set evs \ -\ --> Says Server B \ -\ {|NA, Crypt (shrK A) {|NA, Key K|}, \ -\ Crypt (shrK B) {|NB, Key K|}|} \ +Goal "[| B ~: bad; evs : otway |] \ +\ ==> Crypt (shrK B) {|NB, Key K|} : parts (spies evs) \ +\ --> (ALL X'. Says B Server \ +\ {|NA, Agent A, Agent B, X', \ +\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ +\ : set evs \ +\ --> Says Server B \ +\ {|NA, Crypt (shrK A) {|NA, Key K|}, \ +\ Crypt (shrK B) {|NB, Key K|}|} \ \ : set evs)"; by (parts_induct_tac 1); by (Blast_tac 1); @@ -430,42 +426,39 @@ (*Guarantee for B: if it gets a message with matching NB then the Server has sent the correct message.*) -Goal - "!!evs. [| Says B Server {|NA, Agent A, Agent B, X', \ -\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ -\ : set evs; \ -\ Says S' 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"; +Goal "[| Says B Server {|NA, Agent A, Agent B, X', \ +\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ +\ : set evs; \ +\ Says S' 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"; by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1); qed "B_trusts_OR3"; (*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*) -Goal - "!!evs. [| Says B Server {|NA, Agent A, Agent B, X', \ -\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ -\ : set evs; \ -\ Says S' 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 |] \ -\ ==> Key K ~: analz (spies evs)"; +Goal "[| Says B Server {|NA, Agent A, Agent B, X', \ +\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ +\ : set evs; \ +\ Says S' 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 |] \ +\ ==> Key K ~: analz (spies evs)"; by (blast_tac (claset() addSDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1); qed "B_gets_good_key"; -Goal - "!!evs. [| B ~: bad; evs : otway |] \ -\ ==> Says Server B \ -\ {|NA, Crypt (shrK A) {|NA, Key K|}, \ -\ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \ -\ (EX X. Says B Server {|NA, Agent A, Agent B, X, \ -\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ -\ : set evs)"; +Goal "[| B ~: bad; evs : otway |] \ +\ ==> Says Server B \ +\ {|NA, Crypt (shrK A) {|NA, Key K|}, \ +\ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \ +\ (EX X. Says B Server {|NA, Agent A, Agent B, X, \ +\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ +\ : set evs)"; by (etac otway.induct 1); by (ALLGOALS Asm_simp_tac); by (blast_tac (claset() addSEs [Crypt_imp_OR2]) 3); @@ -476,14 +469,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 - "!!evs. [| Says B' 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 |] \ -\ ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X, \ -\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}\ -\ : set evs"; +Goal "[| Says B' 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 |] \ +\ ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X, \ +\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}\ +\ : set evs"; by (blast_tac (claset() addSDs [A_trusts_OR4] addSEs [OR3_imp_OR2]) 1); qed "A_auths_B"; diff -r c4da11bb0592 -r c729d4c299c1 src/HOL/Auth/OtwayRees_AN.ML --- a/src/HOL/Auth/OtwayRees_AN.ML Thu Jul 02 17:27:35 1998 +0200 +++ b/src/HOL/Auth/OtwayRees_AN.ML Thu Jul 02 17:48:11 1998 +0200 @@ -24,10 +24,10 @@ (*A "possibility property": there are traces that reach the end*) Goal - "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ -\ ==> EX K. EX NA. EX evs: otway. \ -\ Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \ -\ : set evs"; + "[| A ~= B; A ~= Server; B ~= Server |] \ +\ ==> EX K. EX NA. EX evs: otway. \ +\ Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \ +\ : set evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2); by possibility_tac; @@ -37,7 +37,7 @@ (**** Inductive proofs about otway ****) (*Nobody sends themselves messages*) -Goal "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs"; +Goal "evs : otway ==> ALL A X. Says A A X ~: set evs"; by (etac otway.induct 1); by Auto_tac; qed_spec_mp "not_Says_to_self"; @@ -47,14 +47,14 @@ (** For reasoning about the encrypted portion of messages **) -Goal "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \ -\ X : analz (spies evs)"; +Goal "Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \ +\ X : analz (spies evs)"; by (dtac (Says_imp_spies RS analz.Inj) 1); by (Blast_tac 1); qed "OR4_analz_spies"; -Goal "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \ -\ : set evs ==> K : parts (spies evs)"; +Goal "Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \ +\ : set evs ==> K : parts (spies evs)"; by (Blast_tac 1); qed "Oops_parts_spies"; @@ -73,15 +73,13 @@ sends messages containing X! **) (*Spy never sees a good agent's shared key!*) -Goal - "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; +Goal "evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; by (parts_induct_tac 1); by (ALLGOALS Blast_tac); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; -Goal - "!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; +Goal "evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); qed "Spy_analz_shrK"; Addsimps [Spy_analz_shrK]; @@ -91,8 +89,7 @@ (*Nobody can have used non-existent keys!*) -Goal "!!evs. 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); @@ -111,13 +108,12 @@ (*** Proofs involving analz ***) (*Describes the form of K and NA when the Server sends this message.*) -Goal - "!!evs. [| Says Server B \ -\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ -\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ -\ : set evs; \ -\ evs : otway |] \ -\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; +Goal "[| Says Server B \ +\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ +\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ +\ : set evs; \ +\ 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); by (ALLGOALS Asm_simp_tac); @@ -146,11 +142,10 @@ (** Session keys are not used to encrypt other session keys **) (*The equality makes the induction hypothesis easier to apply*) -Goal - "!!evs. evs : otway ==> \ +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))"; +\ (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])); @@ -161,23 +156,21 @@ qed_spec_mp "analz_image_freshK"; -Goal - "!!evs. [| 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"; (*** The Key K uniquely identifies the Server's message. **) -Goal - "!!evs. evs : otway ==> \ -\ EX A' B' NA' NB'. ALL A B NA NB. \ -\ Says Server B \ -\ {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, \ -\ Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set evs \ -\ --> A=A' & B=B' & NA=NA' & NB=NB'"; +Goal "evs : otway ==> \ +\ EX A' B' NA' NB'. ALL A B NA NB. \ +\ Says Server B \ +\ {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, \ +\ Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set evs \ +\ --> A=A' & B=B' & NA=NA' & NB=NB'"; by (etac otway.induct 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); by (ALLGOALS Clarify_tac); @@ -191,17 +184,16 @@ val lemma = result(); -Goal -"!!evs. [| Says Server B \ -\ {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, \ -\ Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} \ -\ : set evs; \ -\ Says Server B' \ -\ {|Crypt (shrK A') {|NA', Agent A', Agent B', K|}, \ -\ Crypt (shrK B') {|NB', Agent A', Agent B', K|}|} \ -\ : set evs; \ -\ evs : otway |] \ -\ ==> A=A' & B=B' & NA=NA' & NB=NB'"; +Goal "[| Says Server B \ +\ {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, \ +\ Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} \ +\ : set evs; \ +\ Says Server B' \ +\ {|Crypt (shrK A') {|NA', Agent A', Agent B', K|}, \ +\ Crypt (shrK B') {|NB', Agent A', Agent B', K|}|} \ +\ : set evs; \ +\ evs : otway |] \ +\ ==> A=A' & B=B' & NA=NA' & NB=NB'"; by (prove_unique_tac lemma 1); qed "unique_session_keys"; @@ -210,13 +202,12 @@ (**** Authenticity properties relating to NA ****) (*If the encrypted message appears then it originated with the Server!*) -Goal - "!!evs. [| A ~: bad; evs : otway |] \ +Goal "[| A ~: bad; evs : otway |] \ \ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} : parts (spies evs) \ -\ --> (EX NB. Says Server B \ -\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ -\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ -\ : set evs)"; +\ --> (EX NB. Says Server B \ +\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ +\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ +\ : set evs)"; by (parts_induct_tac 1); by (Blast_tac 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); @@ -227,14 +218,13 @@ (*Corollary: if A receives B's OR4 message then it originated with the Server. Freshness may be inferred from nonce NA.*) -Goal - "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \ -\ : set evs; \ -\ A ~: bad; evs : otway |] \ -\ ==> EX NB. Says Server B \ -\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ -\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ -\ : set evs"; +Goal "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \ +\ : set evs; \ +\ A ~: bad; evs : otway |] \ +\ ==> EX NB. Says Server B \ +\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ +\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ +\ : set evs"; by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1); qed "A_trusts_OR4"; @@ -243,14 +233,13 @@ Does not in itself guarantee security: an attack could violate the premises, e.g. by having A=Spy **) -Goal - "!!evs. [| A ~: bad; B ~: bad; evs : otway |] \ -\ ==> Says Server B \ -\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ -\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ -\ : set evs --> \ -\ Notes Spy {|NA, NB, Key K|} ~: set evs --> \ -\ Key K ~: analz (spies evs)"; +Goal "[| A ~: bad; B ~: bad; evs : otway |] \ +\ ==> Says Server B \ +\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ +\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ +\ : set evs --> \ +\ Notes Spy {|NA, NB, Key K|} ~: set evs --> \ +\ Key K ~: analz (spies evs)"; by (etac otway.induct 1); by analz_spies_tac; by (ALLGOALS @@ -267,14 +256,13 @@ by (spy_analz_tac 1); val lemma = result() RS mp RS mp RSN(2,rev_notE); -Goal - "!!evs. [| Says Server B \ -\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ -\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ -\ : set evs; \ -\ Notes Spy {|NA, NB, Key K|} ~: set evs; \ -\ A ~: bad; B ~: bad; evs : otway |] \ -\ ==> Key K ~: analz (spies evs)"; +Goal "[| Says Server B \ +\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ +\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ +\ : set evs; \ +\ Notes Spy {|NA, NB, Key K|} ~: set evs; \ +\ A ~: bad; B ~: bad; evs : otway |] \ +\ ==> Key K ~: analz (spies 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"; @@ -282,12 +270,11 @@ (*A's guarantee. The Oops premise quantifies over NB because A cannot know what it is.*) -Goal - "!!evs. [| Says B' 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; evs : otway |] \ -\ ==> Key K ~: analz (spies evs)"; +Goal "[| Says B' 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; evs : otway |] \ +\ ==> Key K ~: analz (spies evs)"; by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1); qed "A_gets_good_key"; @@ -295,13 +282,12 @@ (**** Authenticity properties relating to NB ****) (*If the encrypted message appears then it originated with the Server!*) -Goal - "!!evs. [| B ~: bad; evs : otway |] \ -\ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} : parts (spies evs) \ -\ --> (EX NA. Says Server B \ -\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ -\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ -\ : set evs)"; +Goal "[| B ~: bad; evs : otway |] \ +\ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} : parts (spies evs) \ +\ --> (EX NA. Says Server B \ +\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ +\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ +\ : set evs)"; by (parts_induct_tac 1); by (Blast_tac 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); @@ -312,24 +298,22 @@ (*Guarantee for B: if it gets a well-formed certificate then the Server has sent the correct message in round 3.*) -Goal - "!!evs. [| Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ -\ : set evs; \ -\ B ~: bad; evs : otway |] \ -\ ==> EX NA. Says Server B \ -\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ -\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ -\ : set evs"; +Goal "[| Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ +\ : set evs; \ +\ B ~: bad; evs : otway |] \ +\ ==> EX NA. Says Server B \ +\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ +\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ +\ : set evs"; by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1); qed "B_trusts_OR3"; (*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*) -Goal - "!!evs. [| Says S' 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; evs : otway |] \ -\ ==> Key K ~: analz (spies evs)"; +Goal "[| Says S' 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; evs : otway |] \ +\ ==> Key K ~: analz (spies evs)"; by (blast_tac (claset() addDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1); qed "B_gets_good_key"; diff -r c4da11bb0592 -r c729d4c299c1 src/HOL/Auth/OtwayRees_Bad.ML --- a/src/HOL/Auth/OtwayRees_Bad.ML Thu Jul 02 17:27:35 1998 +0200 +++ b/src/HOL/Auth/OtwayRees_Bad.ML Thu Jul 02 17:48:11 1998 +0200 @@ -27,10 +27,10 @@ (*A "possibility property": there are traces that reach the end*) Goal - "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ -\ ==> EX K. EX NA. EX evs: otway. \ -\ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \ -\ : set evs"; + "[| A ~= B; A ~= Server; B ~= Server |] \ +\ ==> EX K. EX NA. EX evs: otway. \ +\ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \ +\ : set evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2); by possibility_tac; @@ -40,7 +40,7 @@ (**** Inductive proofs about otway ****) (*Nobody sends themselves messages*) -Goal "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs"; +Goal "evs : otway ==> ALL A X. Says A A X ~: set evs"; by (etac otway.induct 1); by Auto_tac; qed_spec_mp "not_Says_to_self"; @@ -50,20 +50,20 @@ (** For reasoning about the encrypted portion of messages **) -Goal "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \ -\ ==> X : analz (spies evs)"; +Goal "Says A' B {|N, Agent A, Agent B, X|} : set evs \ +\ ==> X : analz (spies evs)"; by (dtac (Says_imp_spies RS analz.Inj) 1); by (Blast_tac 1); qed "OR2_analz_spies"; -Goal "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \ -\ ==> X : analz (spies evs)"; +Goal "Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \ +\ ==> X : analz (spies evs)"; by (dtac (Says_imp_spies RS analz.Inj) 1); by (Blast_tac 1); qed "OR4_analz_spies"; -Goal "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \ -\ ==> K : parts (spies evs)"; +Goal "Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \ +\ ==> K : parts (spies evs)"; by (Blast_tac 1); qed "Oops_parts_spies"; @@ -85,15 +85,13 @@ sends messages containing X! **) (*Spy never sees a good agent's shared key!*) -Goal - "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; +Goal "evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; by (parts_induct_tac 1); by (ALLGOALS Blast_tac); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; -Goal - "!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; +Goal "evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); qed "Spy_analz_shrK"; Addsimps [Spy_analz_shrK]; @@ -103,8 +101,7 @@ (*Nobody can have used non-existent keys!*) -Goal "!!evs. 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); @@ -124,10 +121,9 @@ (*Describes the form of K and NA when the Server sends this message. Also for Oops case.*) -Goal - "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \ -\ evs : otway |] \ -\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; +Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \ +\ 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); by (ALLGOALS Simp_tac); @@ -156,11 +152,10 @@ (** Session keys are not used to encrypt other session keys **) (*The equality makes the induction hypothesis easier to apply*) -Goal - "!!evs. 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])); @@ -171,19 +166,17 @@ qed_spec_mp "analz_image_freshK"; -Goal - "!!evs. [| 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"; (*** The Key K uniquely identifies the Server's message. **) -Goal - "!!evs. evs : otway ==> \ -\ EX B' NA' NB' X'. ALL B NA NB X. \ +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 --> \ \ B=B' & NA=NA' & NB=NB' & X=X'"; by (etac otway.induct 1); @@ -198,10 +191,9 @@ by (blast_tac (claset() addSEs spies_partsEs) 1); val lemma = result(); -Goal - "!!evs. [| 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 (prove_unique_tac lemma 1); qed "unique_session_keys"; @@ -210,13 +202,12 @@ Does not in itself guarantee security: an attack could violate the premises, e.g. by having A=Spy **) -Goal - "!!evs. [| A ~: bad; B ~: bad; evs : otway |] \ -\ ==> Says Server B \ -\ {|NA, Crypt (shrK A) {|NA, Key K|}, \ -\ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \ -\ Notes Spy {|NA, NB, Key K|} ~: set evs --> \ -\ Key K ~: analz (spies evs)"; +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 --> \ +\ Notes Spy {|NA, NB, Key K|} ~: set evs --> \ +\ Key K ~: analz (spies evs)"; by (etac otway.induct 1); by analz_spies_tac; by (ALLGOALS @@ -233,13 +224,12 @@ by (spy_analz_tac 1); val lemma = result() RS mp RS mp RSN(2,rev_notE); -Goal - "!!evs. [| Says Server B \ -\ {|NA, Crypt (shrK A) {|NA, Key K|}, \ -\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \ -\ Notes Spy {|NA, NB, Key K|} ~: set evs; \ -\ A ~: bad; B ~: bad; evs : otway |] \ -\ ==> Key K ~: analz (spies evs)"; +Goal "[| Says Server B \ +\ {|NA, Crypt (shrK A) {|NA, Key K|}, \ +\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \ +\ Notes Spy {|NA, NB, Key K|} ~: set evs; \ +\ A ~: bad; B ~: bad; evs : otway |] \ +\ ==> Key K ~: analz (spies 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"; @@ -251,11 +241,10 @@ I'm not sure why A ~= B premise is needed: OtwayRees.ML doesn't need it. Perhaps it's because OR2 has two similar-looking encrypted messages in this version.*) -Goal - "!!evs. [| A ~: bad; A ~= B; evs : otway |] \ -\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \ -\ Says A B {|NA, Agent A, Agent B, \ -\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs"; +Goal "[| A ~: bad; A ~= B; evs : otway |] \ +\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \ +\ Says A B {|NA, Agent A, Agent B, \ +\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs"; by (parts_induct_tac 1); by (ALLGOALS Blast_tac); qed_spec_mp "Crypt_imp_OR1"; @@ -265,16 +254,15 @@ to start a run, then it originated with the Server!*) (*Only it is FALSE. Somebody could make a fake message to Server substituting some other nonce NA' for NB.*) -Goal - "!!evs. [| A ~: bad; evs : otway |] \ -\ ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs) --> \ -\ Says A B {|NA, Agent A, Agent B, \ -\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ -\ : set evs --> \ -\ (EX B NB. Says Server B \ -\ {|NA, \ -\ Crypt (shrK A) {|NA, Key K|}, \ -\ Crypt (shrK B) {|NB, Key K|}|} : set evs)"; +Goal "[| A ~: bad; evs : otway |] \ +\ ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs) --> \ +\ Says A B {|NA, Agent A, Agent B, \ +\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ +\ : set evs --> \ +\ (EX B NB. Says Server B \ +\ {|NA, \ +\ Crypt (shrK A) {|NA, Key K|}, \ +\ Crypt (shrK B) {|NB, Key K|}|} : set evs)"; by (parts_induct_tac 1); (*Fake*) by (Blast_tac 1); diff -r c4da11bb0592 -r c729d4c299c1 src/HOL/Auth/Public.ML --- a/src/HOL/Auth/Public.ML Thu Jul 02 17:27:35 1998 +0200 +++ b/src/HOL/Auth/Public.ML Thu Jul 02 17:48:11 1998 +0200 @@ -15,7 +15,7 @@ AddIffs [inj_pubK RS inj_eq]; -Goal "!!A B. (priK A = priK B) = (A=B)"; +Goal "(priK A = priK B) = (A=B)"; by Safe_tac; by (dres_inst_tac [("f","invKey")] arg_cong 1); by (Full_simp_tac 1); @@ -80,7 +80,7 @@ qed_spec_mp "spies_pubK"; (*Spy sees private keys of bad agents!*) -Goal "!!A. A: bad ==> Key (priK A) : spies evs"; +Goal "A: bad ==> Key (priK A) : spies evs"; by (induct_tac "evs" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [imageI, spies_Cons] @@ -92,8 +92,8 @@ (*For not_bad_tac*) -Goal "!!A. [| Crypt (pubK A) X : analz (spies evs); A: bad |] \ -\ ==> X : analz (spies evs)"; +Goal "[| Crypt (pubK A) X : analz (spies evs); A: bad |] \ +\ ==> X : analz (spies evs)"; by (blast_tac (claset() addSDs [analz.Decrypt]) 1); qed "Crypt_Spy_analz_bad"; diff -r c4da11bb0592 -r c729d4c299c1 src/HOL/Auth/Recur.ML --- a/src/HOL/Auth/Recur.ML Thu Jul 02 17:27:35 1998 +0200 +++ b/src/HOL/Auth/Recur.ML Thu Jul 02 17:48:11 1998 +0200 @@ -20,11 +20,10 @@ (*Simplest case: Alice goes directly to the server*) -Goal - "!!A. A ~= Server \ +Goal "A ~= Server \ \ ==> EX K NA. EX evs: recur. \ -\ Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \ -\ Agent Server|} : set evs"; +\ Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \ +\ Agent Server|} : set evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); by (rtac (recur.Nil RS recur.RA1 RS (respond.One RSN (4,recur.RA3))) 2); @@ -33,11 +32,10 @@ (*Case two: Alice, Bob and the server*) -Goal - "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ +Goal "[| A ~= B; A ~= Server; B ~= Server |] \ \ ==> EX K. EX NA. EX evs: recur. \ -\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \ -\ Agent Server|} : set evs"; +\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \ +\ Agent Server|} : set evs"; by (cut_facts_tac [Nonce_supply2, Key_supply2] 1); by (REPEAT (eresolve_tac [exE, conjE] 1)); by (REPEAT (resolve_tac [exI,bexI] 1)); @@ -52,11 +50,10 @@ (*Case three: Alice, Bob, Charlie and the server TOO SLOW to run every time! -Goal - "!!A B. [| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |] \ +Goal "[| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |] \ \ ==> EX K. EX NA. EX evs: recur. \ -\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \ -\ Agent Server|} : set evs"; +\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \ +\ Agent Server|} : set evs"; by (cut_facts_tac [Nonce_supply3, Key_supply3] 1); by (REPEAT (eresolve_tac [exE, conjE] 1)); by (REPEAT (resolve_tac [exI,bexI] 1)); @@ -75,7 +72,7 @@ (**** Inductive proofs about recur ****) (*Nobody sends themselves messages*) -Goal "!!evs. evs : recur ==> ALL A X. Says A A X ~: set evs"; +Goal "evs : recur ==> ALL A X. Says A A X ~: set evs"; by (etac recur.induct 1); by Auto_tac; qed_spec_mp "not_Says_to_self"; @@ -84,19 +81,18 @@ -Goal "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB : parts{RB}"; +Goal "(PA,RB,KAB) : respond evs ==> Key KAB : parts{RB}"; by (etac respond.induct 1); by (ALLGOALS Simp_tac); qed "respond_Key_in_parts"; -Goal "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB ~: used evs"; +Goal "(PA,RB,KAB) : respond evs ==> Key KAB ~: used evs"; by (etac respond.induct 1); by (REPEAT (assume_tac 1)); qed "respond_imp_not_used"; -Goal - "!!evs. [| Key K : parts {RB}; (PB,RB,K') : respond evs |] \ -\ ==> Key K ~: used evs"; +Goal "[| Key K : parts {RB}; (PB,RB,K') : respond evs |] \ +\ ==> Key K ~: used evs"; by (etac rev_mp 1); by (etac respond.induct 1); by (auto_tac(claset() addDs [Key_not_used, respond_imp_not_used], @@ -104,7 +100,7 @@ qed_spec_mp "Key_in_parts_respond"; (*Simple inductive reasoning about responses*) -Goal "!!evs. (PA,RB,KAB) : respond evs ==> RB : responses evs"; +Goal "(PA,RB,KAB) : respond evs ==> RB : responses evs"; by (etac respond.induct 1); by (REPEAT (ares_tac (respond_imp_not_used::responses.intrs) 1)); qed "respond_imp_responses"; @@ -114,8 +110,8 @@ val RA2_analz_spies = Says_imp_spies RS analz.Inj |> standard; -Goal "!!evs. 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"; @@ -144,8 +140,7 @@ (** Spy never sees another agent's shared key! (unless it's bad at start) **) -Goal - "!!evs. evs : recur ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; +Goal "evs : recur ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); by (ALLGOALS @@ -155,8 +150,7 @@ qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; -Goal - "!!evs. evs : recur ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; +Goal "evs : recur ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); qed "Spy_analz_shrK"; Addsimps [Spy_analz_shrK]; @@ -168,17 +162,16 @@ (** Nobody can have used non-existent keys! **) (*The special case of H={} has the same proof*) -Goal - "!!evs. [| K : keysFor (parts (insert RB H)); (PB,RB,K') : respond evs |] \ -\ ==> K : range shrK | K : keysFor (parts H)"; +Goal "[| K : keysFor (parts (insert RB H)); (PB,RB,K') : respond evs |] \ +\ ==> K : range shrK | K : keysFor (parts H)"; by (etac rev_mp 1); by (etac (respond_imp_responses RS responses.induct) 1); by Auto_tac; qed_spec_mp "Key_in_keysFor_parts"; -Goal "!!evs. 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); @@ -209,24 +202,22 @@ (*Version for "responses" relation. Handles case RA3 in the theorem below. Note that it holds for *any* set H (not just "spies evs") satisfying the inductive hypothesis.*) -Goal - "!!evs. [| RB : responses evs; \ -\ ALL K KK. KK <= Compl (range shrK) --> \ -\ (Key K : analz (Key``KK Un H)) = \ -\ (K : KK | Key K : analz H) |] \ -\ ==> ALL K KK. KK <= Compl (range shrK) --> \ -\ (Key K : analz (insert RB (Key``KK Un H))) = \ -\ (K : KK | Key K : analz (insert RB H))"; +Goal "[| RB : responses evs; \ +\ ALL K KK. KK <= Compl (range shrK) --> \ +\ (Key K : analz (Key``KK Un H)) = \ +\ (K : KK | Key K : analz H) |] \ +\ ==> ALL K KK. KK <= Compl (range shrK) --> \ +\ (Key K : analz (insert RB (Key``KK Un H))) = \ +\ (K : KK | Key K : analz (insert RB H))"; by (etac responses.induct 1); by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); qed "resp_analz_image_freshK_lemma"; (*Version for the protocol. Proof is almost trivial, thanks to the lemma.*) -Goal - "!!evs. evs : recur ==> \ +Goal "evs : recur ==> \ \ ALL K KK. KK <= Compl (range shrK) --> \ -\ (Key K : analz (Key``KK Un (spies evs))) = \ -\ (K : KK | Key K : analz (spies evs))"; +\ (Key K : analz (Key``KK Un (spies evs))) = \ +\ (K : KK | Key K : analz (spies evs))"; by (etac recur.induct 1); by analz_spies_tac; by (REPEAT_FIRST (resolve_tac [allI, impI])); @@ -250,18 +241,17 @@ raw_analz_image_freshK RSN (2, resp_analz_image_freshK_lemma) RS spec RS spec RS mp); -Goal - "!!evs. [| evs : recur; KAB ~: range shrK |] ==> \ -\ Key K : analz (insert (Key KAB) (spies evs)) = \ -\ (K = KAB | Key K : analz (spies evs))"; +Goal "[| evs : recur; 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"; (*Everything that's hashed is already in past traffic. *) -Goal "!!evs. [| Hash {|Key(shrK A), X|} : parts (spies evs); \ -\ evs : recur; A ~: bad |] \ -\ ==> X : parts (spies evs)"; +Goal "[| Hash {|Key(shrK A), 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*) @@ -278,11 +268,10 @@ Unicity is not used in other proofs but is desirable in its own right. **) -Goal - "!!evs. [| evs : recur; A ~: bad |] \ +Goal "[| evs : recur; A ~: bad |] \ \ ==> EX B' P'. ALL B P. \ -\ Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (spies evs) \ -\ --> B=B' & P=P'"; +\ 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 (etac responses.induct 3); @@ -296,10 +285,10 @@ val lemma = result(); Goalw [HPair_def] - "!!A.[| Hash[Key(shrK A)] {|Agent A, B,NA,P|} : parts (spies evs); \ -\ Hash[Key(shrK A)] {|Agent A, B',NA,P'|} : parts (spies evs); \ -\ evs : recur; A ~: bad |] \ -\ ==> B=B' & P=P'"; + "[| Hash[Key(shrK A)] {|Agent A, B,NA,P|} : parts (spies evs); \ +\ Hash[Key(shrK A)] {|Agent A, B',NA,P'|} : parts (spies evs); \ +\ evs : recur; A ~: bad |] \ +\ ==> B=B' & P=P'"; by (REPEAT (eresolve_tac partsEs 1)); by (prove_unique_tac lemma 1); qed "unique_NA"; @@ -309,8 +298,7 @@ (relations "respond" and "responses") ***) -Goal - "!!evs. [| RB : responses evs; evs : recur |] \ +Goal "[| RB : responses evs; evs : recur |] \ \ ==> (Key (shrK B) : analz (insert RB (spies evs))) = (B:bad)"; by (etac responses.induct 1); by (ALLGOALS @@ -321,13 +309,12 @@ Addsimps [shrK_in_analz_respond]; -Goal - "!!evs. [| RB : responses evs; \ -\ ALL K KK. KK <= Compl (range shrK) --> \ -\ (Key K : analz (Key``KK Un H)) = \ -\ (K : KK | Key K : analz H) |] \ -\ ==> (Key K : analz (insert RB H)) --> \ -\ (Key K : parts{RB} | Key K : analz H)"; +Goal "[| RB : responses evs; \ +\ ALL K KK. KK <= Compl (range shrK) --> \ +\ (Key K : analz (Key``KK Un H)) = \ +\ (K : KK | Key K : analz H) |] \ +\ ==> (Key K : analz (insert RB H)) --> \ +\ (Key K : parts{RB} | Key K : analz H)"; by (etac responses.induct 1); by (ALLGOALS (asm_simp_tac @@ -344,9 +331,8 @@ (*The Server does not send such messages. This theorem lets us avoid assuming B~=Server in RA4.*) -Goal - "!!evs. evs : recur \ -\ ==> ALL C X Y. Says Server C {|X, Agent Server, Y|} ~: set evs"; +Goal "evs : recur \ +\ ==> ALL C X Y. Says Server C {|X, Agent Server, Y|} ~: set evs"; by (etac recur.induct 1); by (etac (respond.induct) 5); by Auto_tac; @@ -355,19 +341,17 @@ (*The last key returned by respond indeed appears in a certificate*) -Goal - "!!K. (Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) : respond evs \ -\ ==> Crypt (shrK A) {|Key K, B, NA|} : parts {RA}"; +Goal "(Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) : respond evs \ +\ ==> Crypt (shrK A) {|Key K, B, NA|} : parts {RA}"; by (etac respond.elim 1); by (ALLGOALS Asm_full_simp_tac); qed "respond_certificate"; -Goal - "!!K'. (PB,RB,KXY) : respond evs \ +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)"; +\ 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*) @@ -385,10 +369,9 @@ by (Fast_tac 1); val lemma = result(); -Goal - "!!RB. [| 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 |] \ +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)"; by (prove_unique_tac lemma 1); qed "unique_session_keys"; @@ -398,11 +381,10 @@ Does not in itself guarantee security: an attack could violate the premises, e.g. by having A=Spy **) -Goal - "!!evs. [| (PB,RB,KAB) : respond evs; evs : recur |] \ -\ ==> ALL A A' N. A ~: bad & A' ~: bad --> \ -\ Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} --> \ -\ Key K ~: analz (insert RB (spies evs))"; +Goal "[| (PB,RB,KAB) : respond evs; evs : recur |] \ +\ ==> ALL A A' N. A ~: bad & A' ~: bad --> \ +\ Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} --> \ +\ Key K ~: analz (insert RB (spies evs))"; by (etac respond.induct 1); by (forward_tac [respond_imp_responses] 2); by (forward_tac [respond_imp_not_used] 2); @@ -429,10 +411,9 @@ qed_spec_mp "respond_Spy_not_see_session_key"; -Goal - "!!evs. [| Crypt (shrK A) {|Key K, Agent A', N|} : parts (spies evs); \ -\ A ~: bad; A' ~: bad; evs : recur |] \ -\ ==> Key K ~: analz (spies evs)"; +Goal "[| Crypt (shrK A) {|Key K, Agent A', N|} : parts (spies evs); \ +\ A ~: bad; A' ~: bad; evs : recur |] \ +\ ==> Key K ~: analz (spies evs)"; by (etac rev_mp 1); by (etac recur.induct 1); by analz_spies_tac; @@ -463,10 +444,9 @@ (**** Authenticity properties for Agents ****) (*The response never contains Hashes*) -Goal - "!!evs. [| Hash {|Key (shrK B), M|} : parts (insert RB H); \ -\ (PB,RB,K) : respond evs |] \ -\ ==> Hash {|Key (shrK B), M|} : parts H"; +Goal "[| Hash {|Key (shrK B), M|} : parts (insert RB H); \ +\ (PB,RB,K) : respond evs |] \ +\ ==> Hash {|Key (shrK B), M|} : parts H"; by (etac rev_mp 1); by (etac (respond_imp_responses RS responses.induct) 1); by Auto_tac; @@ -477,9 +457,9 @@ it can say nothing about how recent A's message is. It might later be used to prove B's presence to A at the run's conclusion.*) Goalw [HPair_def] - "!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} : parts(spies evs); \ -\ A ~: bad; evs : recur |] \ -\ ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) : set evs"; + "[| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} : parts(spies evs); \ +\ A ~: bad; evs : recur |] \ +\ ==> 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); @@ -493,11 +473,10 @@ (*Certificates can only originate with the Server.*) -Goal - "!!evs. [| Crypt (shrK A) Y : parts (spies evs); \ -\ A ~: bad; evs : recur |] \ -\ ==> EX C RC. Says Server C RC : set evs & \ -\ Crypt (shrK A) Y : parts {RC}"; +Goal "[| Crypt (shrK A) Y : parts (spies evs); \ +\ A ~: bad; evs : recur |] \ +\ ==> EX C RC. Says Server C RC : set evs & \ +\ Crypt (shrK A) Y : parts {RC}"; by (etac rev_mp 1); by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); diff -r c4da11bb0592 -r c729d4c299c1 src/HOL/Auth/Shared.ML --- a/src/HOL/Auth/Shared.ML Thu Jul 02 17:27:35 1998 +0200 +++ b/src/HOL/Auth/Shared.ML Thu Jul 02 17:48:11 1998 +0200 @@ -29,7 +29,7 @@ Addsimps [keysFor_parts_initState]; (*Specialized to shared-key model: no need for addss in protocol proofs*) -Goal "!!X. [| K: keysFor (parts (insert X H)); X : synth (analz H) |] \ +Goal "[| K: keysFor (parts (insert X H)); X : synth (analz H) |] \ \ ==> K : keysFor (parts H) | Key K : parts H"; by (fast_tac (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono), @@ -38,7 +38,7 @@ addss (simpset())) 1); qed "keysFor_parts_insert"; -Goal "!!H. Crypt K X : H ==> K : keysFor H"; +Goal "Crypt K X : H ==> K : keysFor H"; by (dtac Crypt_imp_invKey_keysFor 1); by (Asm_full_simp_tac 1); qed "Crypt_imp_keysFor"; @@ -47,7 +47,7 @@ (*** Function "spies" ***) (*Spy sees shared keys of agents!*) -Goal "!!A. A: bad ==> Key (shrK A) : spies evs"; +Goal "A: bad ==> Key (shrK A) : spies evs"; by (induct_tac "evs" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [imageI, spies_Cons] @@ -57,7 +57,7 @@ AddSIs [Spy_spies_bad]; (*For not_bad_tac*) -Goal "!!A. [| Crypt (shrK A) X : analz (spies evs); A: bad |] \ +Goal "[| Crypt (shrK A) X : analz (spies evs); A: bad |] \ \ ==> X : analz (spies evs)"; by (fast_tac (claset() addSDs [analz.Decrypt] addss (simpset())) 1); qed "Crypt_Spy_analz_bad"; @@ -92,11 +92,11 @@ (*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys from long-term shared keys*) -Goal "!!K. Key K ~: used evs ==> K ~: range shrK"; +Goal "Key K ~: used evs ==> K ~: range shrK"; by (Blast_tac 1); qed "Key_not_used"; -Goal "!!K. Key K ~: used evs ==> shrK B ~= K"; +Goal "Key K ~: used evs ==> shrK B ~= K"; by (Blast_tac 1); qed "shrK_neq"; @@ -223,7 +223,7 @@ (*** Specialized rewriting for analz_insert_freshK ***) -Goal "!!A. A <= Compl (range shrK) ==> shrK x ~: A"; +Goal "A <= Compl (range shrK) ==> shrK x ~: A"; by (Blast_tac 1); qed "subset_Compl_range"; @@ -250,7 +250,7 @@ (*Lemma for the trivial direction of the if-and-only-if*) Goal - "!!evs. (Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H) ==> \ + "(Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H) ==> \ \ (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)"; by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1); qed "analz_image_freshK_lemma"; diff -r c4da11bb0592 -r c729d4c299c1 src/HOL/Auth/TLS.ML --- a/src/HOL/Auth/TLS.ML Thu Jul 02 17:27:35 1998 +0200 +++ b/src/HOL/Auth/TLS.ML Thu Jul 02 17:48:11 1998 +0200 @@ -64,11 +64,10 @@ (*Possibility property ending with ClientAccepts.*) -Goal - "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ -\ A ~= B |] \ +Goal "[| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ +\ A ~= B |] \ \ ==> EX SID M. EX evs: tls. \ -\ Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs"; +\ Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS tls.ClientKeyExch RS tls.ClientFinished RS tls.ServerFinished RS @@ -78,11 +77,10 @@ result(); (*And one for ServerAccepts. Either FINISHED message may come first.*) -Goal - "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ -\ A ~= B |] \ +Goal "[| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ +\ A ~= B |] \ \ ==> EX SID NA PA NB PB M. EX evs: tls. \ -\ Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs"; +\ Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS tls.ClientKeyExch RS tls.ServerFinished RS tls.ClientFinished RS @@ -92,9 +90,8 @@ result(); (*Another one, for CertVerify (which is optional)*) -Goal - "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ -\ A ~= B |] \ +Goal "[| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ +\ A ~= B |] \ \ ==> EX NB PMS. EX evs: tls. \ \ Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|})) : set evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); @@ -105,17 +102,16 @@ result(); (*Another one, for session resumption (both ServerResume and ClientResume) *) -Goal - "!!A B. [| evs0 : tls; \ -\ Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \ -\ Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \ -\ ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ -\ A ~= B |] ==> EX NA PA NB PB X. EX evs: tls. \ -\ X = Hash{|Number SID, Nonce M, \ -\ Nonce NA, Number PA, Agent A, \ -\ Nonce NB, Number PB, Agent B|} & \ -\ Says A B (Crypt (clientK(NA,NB,M)) X) : set evs & \ -\ Says B A (Crypt (serverK(NA,NB,M)) X) : set evs"; +Goal "[| evs0 : tls; \ +\ Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \ +\ Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \ +\ ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ +\ A ~= B |] ==> EX NA PA NB PB X. EX evs: tls. \ +\ X = Hash{|Number SID, Nonce M, \ +\ Nonce NA, Number PA, Agent A, \ +\ Nonce NB, Number PB, Agent B|} & \ +\ Says A B (Crypt (clientK(NA,NB,M)) X) : set evs & \ +\ Says B A (Crypt (serverK(NA,NB,M)) X) : set evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); by (etac (tls.ClientHello RS tls.ServerHello RS tls.ServerResume RS tls.ClientResume) 2); @@ -128,7 +124,7 @@ (**** Inductive proofs about tls ****) (*Nobody sends themselves messages*) -Goal "!!evs. evs : tls ==> ALL A X. Says A A X ~: set evs"; +Goal "evs : tls ==> ALL A X. Says A A X ~: set evs"; by (etac tls.induct 1); by Auto_tac; qed_spec_mp "not_Says_to_self"; @@ -152,15 +148,13 @@ sends messages containing X! **) (*Spy never sees another agent's private key! (unless it's bad at start)*) -Goal - "!!evs. evs : tls ==> (Key (priK A) : parts (spies evs)) = (A : bad)"; +Goal "evs : tls ==> (Key (priK A) : parts (spies evs)) = (A : bad)"; by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); qed "Spy_see_priK"; Addsimps [Spy_see_priK]; -Goal - "!!evs. evs : tls ==> (Key (priK A) : analz (spies evs)) = (A : bad)"; +Goal "evs : tls ==> (Key (priK A) : analz (spies evs)) = (A : bad)"; by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); qed "Spy_analz_priK"; Addsimps [Spy_analz_priK]; @@ -174,8 +168,8 @@ little point in doing so: the loss of their private keys is a worse breach of security.*) Goalw [certificate_def] - "!!evs. [| 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); @@ -203,18 +197,17 @@ (*** Properties of items found in Notes ***) -Goal "!!evs. [| Notes A {|Agent B, X|} : set evs; evs : tls |] \ -\ ==> Crypt (pubK B) X : parts (spies evs)"; +Goal "[| Notes A {|Agent B, X|} : set evs; evs : tls |] \ +\ ==> 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); qed "Notes_Crypt_parts_spies"; (*C may be either A or B*) -Goal - "!!evs. [| Notes C {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} : set evs; \ -\ evs : tls \ -\ |] ==> Crypt (pubK B) (Nonce PMS) : parts (spies evs)"; +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)"; by (etac rev_mp 1); by (parts_induct_tac 1); by (ALLGOALS Clarify_tac); @@ -226,10 +219,9 @@ qed "Notes_master_imp_Crypt_PMS"; (*Compared with the theorem above, both premise and conclusion are stronger*) -Goal - "!!evs. [| Notes A {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} : set evs;\ -\ evs : tls \ -\ |] ==> Notes A {|Agent B, Nonce PMS|} : set evs"; +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"; by (etac rev_mp 1); by (parts_induct_tac 1); (*ServerAccepts*) @@ -240,11 +232,10 @@ (*** Protocol goal: if B receives CertVerify, then A sent it ***) (*B can check A's signature if he has received A's certificate.*) -Goal - "!!evs. [| X : parts (spies evs); \ -\ X = Crypt (priK A) (Hash{|nb, Agent B, pms|}); \ -\ evs : tls; A ~: bad |] \ -\ ==> Says A B X : set evs"; +Goal "[| X : parts (spies evs); \ +\ X = Crypt (priK A) (Hash{|nb, Agent B, pms|}); \ +\ evs : tls; A ~: bad |] \ +\ ==> Says A B X : set evs"; by (etac rev_mp 1); by (hyp_subst_tac 1); by (parts_induct_tac 1); @@ -252,39 +243,36 @@ val lemma = result(); (*Final version: B checks X using the distributed KA instead of priK A*) -Goal - "!!evs. [| X : parts (spies evs); \ -\ 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"; +Goal "[| X : parts (spies evs); \ +\ 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"; by (blast_tac (claset() addSDs [certificate_valid] addSIs [lemma]) 1); qed "TrustCertVerify"; (*If CertVerify is present then A has chosen PMS.*) -Goal - "!!evs. [| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|}) \ -\ : parts (spies evs); \ -\ evs : tls; A ~: bad |] \ -\ ==> Notes A {|Agent B, Nonce PMS|} : set evs"; +Goal "[| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|}) \ +\ : parts (spies evs); \ +\ evs : tls; A ~: bad |] \ +\ ==> Notes A {|Agent B, Nonce PMS|} : set evs"; by (etac rev_mp 1); by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); val lemma = result(); (*Final version using the distributed KA instead of priK A*) -Goal - "!!evs. [| Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}) \ -\ : parts (spies evs); \ -\ certificate A KA : parts (spies evs); \ -\ evs : tls; A ~: bad |] \ -\ ==> Notes A {|Agent B, Nonce PMS|} : set evs"; +Goal "[| Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}) \ +\ : parts (spies evs); \ +\ certificate A KA : parts (spies evs); \ +\ evs : tls; A ~: bad |] \ +\ ==> Notes A {|Agent B, Nonce PMS|} : set evs"; by (blast_tac (claset() addSDs [certificate_valid] addSIs [lemma]) 1); qed "UseCertVerify"; -Goal "!!evs. evs : tls ==> Notes A {|Agent B, Nonce (PRF x)|} ~: set evs"; +Goal "evs : tls ==> Notes A {|Agent B, Nonce (PRF x)|} ~: set evs"; by (parts_induct_tac 1); (*ClientKeyExch: PMS is assumed to differ from any PRF.*) by (Blast_tac 1); @@ -292,9 +280,9 @@ Addsimps [no_Notes_A_PRF]; -Goal "!!evs. [| 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); @@ -309,10 +297,9 @@ (*** Unicity results for PMS, the pre-master-secret ***) (*PMS determines B. Proof borrowed from NS_Public/unique_NA and from Yahalom*) -Goal - "!!evs. [| Nonce PMS ~: analz (spies evs); evs : tls |] \ -\ ==> EX B'. ALL B. \ -\ Crypt (pubK B) (Nonce PMS) : parts (spies evs) --> B=B'"; +Goal "[| Nonce PMS ~: analz (spies evs); evs : tls |] \ +\ ==> EX B'. ALL B. \ +\ Crypt (pubK B) (Nonce PMS) : parts (spies evs) --> B=B'"; by (etac rev_mp 1); by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); @@ -323,12 +310,11 @@ blast_tac (claset() addSEs partsEs) 1); val lemma = result(); -Goal - "!!evs. [| Crypt(pubK B) (Nonce PMS) : parts (spies evs); \ -\ Crypt(pubK B') (Nonce PMS) : parts (spies evs); \ -\ Nonce PMS ~: analz (spies evs); \ -\ evs : tls |] \ -\ ==> B=B'"; +Goal "[| Crypt(pubK B) (Nonce PMS) : parts (spies evs); \ +\ Crypt(pubK B') (Nonce PMS) : parts (spies evs); \ +\ Nonce PMS ~: analz (spies evs); \ +\ evs : tls |] \ +\ ==> B=B'"; by (prove_unique_tac lemma 1); qed "Crypt_unique_PMS"; @@ -340,9 +326,9 @@ **) (*In A's internal Note, PMS determines A and B.*) -Goal "!!evs. 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.*) @@ -350,11 +336,10 @@ blast_tac (claset() addSDs [Notes_Crypt_parts_spies] addSEs partsEs) 1); val lemma = result(); -Goal - "!!evs. [| Notes A {|Agent B, Nonce PMS|} : set evs; \ -\ Notes A' {|Agent B', Nonce PMS|} : set evs; \ -\ evs : tls |] \ -\ ==> A=A' & B=B'"; +Goal "[| Notes A {|Agent B, Nonce PMS|} : set evs; \ +\ Notes A' {|Agent B', Nonce PMS|} : set evs; \ +\ evs : tls |] \ +\ ==> A=A' & B=B'"; by (prove_unique_tac lemma 1); qed "Notes_unique_PMS"; @@ -364,10 +349,9 @@ (*Key compromise lemma needed to prove analz_image_keys. No collection of keys can help the spy get new private keys.*) -Goal - "!!evs. evs : tls ==> \ +Goal "evs : tls ==> \ \ ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \ -\ (priK B : KK | B : bad)"; +\ (priK B : KK | B : bad)"; by (etac tls.induct 1); by (ALLGOALS (asm_simp_tac (analz_image_keys_ss @@ -378,27 +362,25 @@ (*slightly speeds up the big simplification below*) -Goal "!!evs. KK <= range sessionK ==> priK B ~: KK"; +Goal "KK <= range sessionK ==> priK B ~: KK"; by (Blast_tac 1); val range_sessionkeys_not_priK = result(); (*Lemma for the trivial direction of the if-and-only-if*) -Goal - "!!evs. (X : analz (G Un H)) --> (X : analz H) ==> \ -\ (X : analz (G Un H)) = (X : analz H)"; +Goal "(X : analz (G Un H)) --> (X : analz H) ==> \ +\ (X : analz (G Un H)) = (X : analz H)"; by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1); val analz_image_keys_lemma = result(); (** Strangely, the following version doesn't work: -\ ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \ -\ (Nonce N : analz (spies evs))"; +\ ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \ +\ (Nonce N : analz (spies evs))"; **) -Goal - "!!evs. evs : tls ==> \ -\ ALL KK. KK <= range sessionK --> \ -\ (Nonce N : analz (Key``KK Un (spies evs))) = \ -\ (Nonce N : analz (spies evs))"; +Goal "evs : tls ==> \ +\ ALL KK. KK <= range sessionK --> \ +\ (Nonce N : analz (Key``KK Un (spies evs))) = \ +\ (Nonce N : analz (spies evs))"; by (etac tls.induct 1); by (ClientKeyExch_tac 7); by (REPEAT_FIRST (resolve_tac [allI, impI])); @@ -414,10 +396,9 @@ qed_spec_mp "analz_image_keys"; (*Knowing some session keys is no help in getting new nonces*) -Goal - "!!evs. evs : tls ==> \ -\ Nonce N : analz (insert (Key (sessionK z)) (spies evs)) = \ -\ (Nonce N : analz (spies evs))"; +Goal "evs : tls ==> \ +\ Nonce N : analz (insert (Key (sessionK z)) (spies evs)) = \ +\ (Nonce N : analz (spies evs))"; by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 1); qed "analz_insert_key"; Addsimps [analz_insert_key]; @@ -432,10 +413,9 @@ Nonces don't have to agree, allowing session resumption. Converse doesn't hold; revealing PMS doesn't force the keys to be sent. THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*) -Goal - "!!evs. [| Nonce PMS ~: parts (spies evs); \ -\ K = sessionK((Na, Nb, PRF(PMS,NA,NB)), b); \ -\ evs : tls |] \ +Goal "[| Nonce PMS ~: parts (spies evs); \ +\ K = sessionK((Na, Nb, PRF(PMS,NA,NB)), b); \ +\ evs : tls |] \ \ ==> Key K ~: parts (spies evs) & (ALL Y. Crypt K Y ~: parts (spies evs))"; by (etac rev_mp 1); by (hyp_subst_tac 1); @@ -455,17 +435,15 @@ addSEs spies_partsEs) 1)); val lemma = result(); -Goal - "!!evs. [| Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) : parts (spies evs); \ -\ evs : tls |] \ -\ ==> Nonce PMS : parts (spies evs)"; +Goal "[| Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) : parts (spies evs); \ +\ evs : tls |] \ +\ ==> Nonce PMS : parts (spies evs)"; by (blast_tac (claset() addDs [lemma]) 1); qed "PMS_sessionK_not_spied"; -Goal - "!!evs. [| Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y \ -\ : parts (spies evs); evs : tls |] \ -\ ==> Nonce PMS : parts (spies evs)"; +Goal "[| Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y \ +\ : parts (spies evs); evs : tls |] \ +\ ==> Nonce PMS : parts (spies evs)"; by (blast_tac (claset() addDs [lemma]) 1); qed "PMS_Crypt_sessionK_not_spied"; @@ -473,10 +451,9 @@ Converse doesn't hold; betraying M doesn't force the keys to be sent! The strong Oops condition can be weakened later by unicity reasoning, with some effort.*) -Goal - "!!evs. [| ALL A. Says A Spy (Key (sessionK((NA,NB,M),b))) ~: set evs; \ -\ Nonce M ~: analz (spies evs); evs : tls |] \ -\ ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)"; +Goal "[| ALL A. Says A Spy (Key (sessionK((NA,NB,M),b))) ~: set evs; \ +\ Nonce M ~: analz (spies evs); evs : tls |] \ +\ ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)"; by (etac rev_mp 1); by (etac rev_mp 1); by (analz_induct_tac 1); (*17 seconds*) @@ -491,10 +468,9 @@ (*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*) -Goal - "!!evs. [| evs : tls; A ~: bad; B ~: bad |] \ -\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ -\ Nonce PMS ~: analz (spies evs)"; +Goal "[| evs : tls; A ~: bad; B ~: bad |] \ +\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ +\ Nonce PMS ~: analz (spies evs)"; by (analz_induct_tac 1); (*11 seconds*) (*ClientAccepts and ServerAccepts: because PMS ~: range PRF*) by (REPEAT (fast_tac (claset() addss (simpset())) 6)); @@ -513,10 +489,9 @@ (*If A sends ClientKeyExch to an honest B, then the MASTER SECRET will stay secret.*) -Goal - "!!evs. [| evs : tls; A ~: bad; B ~: bad |] \ -\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ -\ Nonce (PRF(PMS,NA,NB)) ~: analz (spies evs)"; +Goal "[| evs : tls; A ~: bad; B ~: bad |] \ +\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ +\ Nonce (PRF(PMS,NA,NB)) ~: analz (spies evs)"; by (analz_induct_tac 1); (*13 seconds*) (*ClientAccepts and ServerAccepts: because PMS was already visible*) by (REPEAT (blast_tac (claset() addDs [Spy_not_see_PMS, @@ -541,11 +516,10 @@ (*If A created PMS then nobody other than the Spy would send a message using a clientK generated from that PMS.*) -Goal - "!!evs. [| evs : tls; A' ~= Spy |] \ +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'"; +\ 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*) @@ -561,11 +535,10 @@ (*If A created PMS and has not leaked her clientK to the Spy, then nobody has.*) -Goal - "!!evs. evs : tls \ +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) "; +\ 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); @@ -585,11 +558,10 @@ (*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. [| evs : tls; A ~: bad; B ~: bad; B' ~= Spy |] \ +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'"; +\ 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*) @@ -608,11 +580,10 @@ (*If A created PMS for B, and B has not leaked his serverK to the Spy, then nobody has.*) -Goal - "!!evs. [| evs : tls; A ~: bad; B ~: bad |] \ +Goal "[| evs : tls; A ~: bad; B ~: bad |] \ \ ==> Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \ -\ Notes A {|Agent B, Nonce PMS|} : set evs --> \ -\ (ALL A. Says A Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) "; +\ Notes A {|Agent B, Nonce PMS|} : set evs --> \ +\ (ALL A. Says A Spy (Key(serverK(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); @@ -634,42 +605,39 @@ ***) (*The mention of her name (A) in X assures A that B knows who she is.*) -Goal - "!!evs. [| X = Crypt (serverK(Na,Nb,M)) \ -\ (Hash{|Number SID, Nonce M, \ -\ Nonce Na, Number PA, Agent A, \ -\ Nonce Nb, Number PB, Agent B|}); \ -\ M = PRF(PMS,NA,NB); \ -\ evs : tls; A ~: bad; B ~: bad |] \ -\ ==> (ALL A. Says A Spy (Key(serverK(Na,Nb,M))) ~: set evs) --> \ -\ Notes A {|Agent B, Nonce PMS|} : set evs --> \ -\ X : parts (spies evs) --> Says B A X : set evs"; +Goal "[| X = Crypt (serverK(Na,Nb,M)) \ +\ (Hash{|Number SID, Nonce M, \ +\ Nonce Na, Number PA, Agent A, \ +\ Nonce Nb, Number PB, Agent B|}); \ +\ M = PRF(PMS,NA,NB); \ +\ evs : tls; A ~: bad; B ~: bad |] \ +\ ==> (ALL A. Says A Spy (Key(serverK(Na,Nb,M))) ~: set evs) --> \ +\ Notes A {|Agent B, Nonce PMS|} : set evs --> \ +\ X : parts (spies evs) --> Says B A X : set evs"; by (hyp_subst_tac 1); -by (analz_induct_tac 1); (*26 seconds*) +by (analz_induct_tac 1); (*10 seconds*) by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); -(*proves ServerResume*) by (ALLGOALS Clarify_tac); (*ClientKeyExch*) by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied]) 2); (*Fake: the Spy doesn't have the critical session key!*) -by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1); +by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evs)" 1); by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, not_parts_not_analz]) 2); by (Fake_parts_insert_tac 1); val lemma = normalize_thm [RSmp] (result()); (*Final version*) -Goal - "!!evs. [| X = Crypt (serverK(Na,Nb,M)) \ -\ (Hash{|Number SID, Nonce M, \ -\ Nonce Na, Number PA, Agent A, \ -\ Nonce Nb, Number PB, Agent B|}); \ -\ M = PRF(PMS,NA,NB); \ -\ X : parts (spies evs); \ -\ Notes A {|Agent B, Nonce PMS|} : set evs; \ -\ Says B Spy (Key (serverK(Na,Nb,M))) ~: set evs; \ -\ evs : tls; A ~: bad; B ~: bad |] \ -\ ==> Says B A X : set evs"; +Goal "[| X = Crypt (serverK(Na,Nb,M)) \ +\ (Hash{|Number SID, Nonce M, \ +\ Nonce Na, Number PA, Agent A, \ +\ Nonce Nb, Number PB, Agent B|}); \ +\ M = PRF(PMS,NA,NB); \ +\ X : parts (spies evs); \ +\ Notes A {|Agent B, Nonce PMS|} : set evs; \ +\ Says B Spy (Key (serverK(Na,Nb,M))) ~: set evs; \ +\ evs : tls; A ~: bad; B ~: bad |] \ +\ ==> Says B A X : set evs"; by (blast_tac (claset() addIs [lemma] addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1); qed_spec_mp "TrustServerFinished"; @@ -681,12 +649,11 @@ have changed A's identity in all other messages, so we can't be sure that B sends his message to A. If CLIENT KEY EXCHANGE were augmented to bind A's identity with PMS, then we could replace A' by A below.*) -Goal - "!!evs. [| M = PRF(PMS,NA,NB); evs : tls; A ~: bad; B ~: bad |] \ -\ ==> (ALL A. Says A Spy (Key(serverK(Na,Nb,M))) ~: set evs) --> \ -\ Notes A {|Agent B, Nonce PMS|} : set evs --> \ -\ Crypt (serverK(Na,Nb,M)) Y : parts (spies evs) --> \ -\ (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)"; +Goal "[| M = PRF(PMS,NA,NB); evs : tls; A ~: bad; B ~: bad |] \ +\ ==> (ALL A. Says A Spy (Key(serverK(Na,Nb,M))) ~: set evs) --> \ +\ Notes A {|Agent B, Nonce PMS|} : set evs --> \ +\ Crypt (serverK(Na,Nb,M)) Y : parts (spies evs) --> \ +\ (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)"; by (hyp_subst_tac 1); by (analz_induct_tac 1); (*20 seconds*) by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); @@ -702,20 +669,19 @@ (*ClientKeyExch*) by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied]) 2); (*Fake: the Spy doesn't have the critical session key!*) -by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1); +by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evs)" 1); by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, not_parts_not_analz]) 2); by (Fake_parts_insert_tac 1); val lemma = normalize_thm [RSmp] (result()); (*Final version*) -Goal - "!!evs. [| M = PRF(PMS,NA,NB); \ -\ Crypt (serverK(Na,Nb,M)) Y : parts (spies evs); \ -\ Notes A {|Agent B, Nonce PMS|} : set evs; \ -\ Says B Spy (Key (serverK(Na,Nb,M))) ~: set evs; \ -\ evs : tls; A ~: bad; B ~: bad |] \ -\ ==> EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs"; +Goal "[| M = PRF(PMS,NA,NB); \ +\ Crypt (serverK(Na,Nb,M)) Y : parts (spies evs); \ +\ Notes A {|Agent B, Nonce PMS|} : set evs; \ +\ Says B Spy (Key (serverK(Na,Nb,M))) ~: set evs; \ +\ evs : tls; A ~: bad; B ~: bad |] \ +\ ==> EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs"; by (blast_tac (claset() addIs [lemma] addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1); qed_spec_mp "TrustServerMsg"; @@ -728,12 +694,11 @@ ClientFinished, then B can then check the quoted values PA, PB, etc. ***) -Goal - "!!evs. [| 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"; +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"; by (hyp_subst_tac 1); by (analz_induct_tac 1); (*15 seconds*) by (ALLGOALS Clarify_tac); @@ -744,19 +709,18 @@ (*ClientKeyExch*) by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied]) 2); (*Fake: the Spy doesn't have the critical session key!*) -by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1); +by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evs)" 1); by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, not_parts_not_analz]) 2); by (Fake_parts_insert_tac 1); val lemma = normalize_thm [RSmp] (result()); (*Final version*) -Goal - "!!evs. [| M = PRF(PMS,NA,NB); \ -\ Crypt (clientK(Na,Nb,M)) Y : parts (spies evs); \ -\ Notes A {|Agent B, Nonce PMS|} : set evs; \ -\ Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs; \ -\ evs : tls; A ~: bad; B ~: bad |] \ +Goal "[| M = PRF(PMS,NA,NB); \ +\ Crypt (clientK(Na,Nb,M)) Y : parts (spies evs); \ +\ 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"; by (blast_tac (claset() addIs [lemma] addEs [clientK_Oops_ALL RSN(2, rev_notE)]) 1); @@ -768,15 +732,14 @@ check a CertVerify from A, then A has used the quoted values PA, PB, etc. Even this one requires A to be uncompromised. ***) -Goal - "!!evs. [| M = PRF(PMS,NA,NB); \ -\ Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs;\ -\ Says A' B (Crypt (clientK(Na,Nb,M)) Y) : set evs; \ -\ 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"; +Goal "[| M = PRF(PMS,NA,NB); \ +\ Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs;\ +\ Says A' B (Crypt (clientK(Na,Nb,M)) Y) : set evs; \ +\ 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"; by (blast_tac (claset() addSIs [TrustClientMsg, UseCertVerify] addDs [Says_imp_spies RS parts.Inj]) 1); qed "AuthClientFinished"; diff -r c4da11bb0592 -r c729d4c299c1 src/HOL/Auth/WooLam.ML --- a/src/HOL/Auth/WooLam.ML Thu Jul 02 17:27:35 1998 +0200 +++ b/src/HOL/Auth/WooLam.ML Thu Jul 02 17:48:11 1998 +0200 @@ -21,10 +21,9 @@ (*A "possibility property": there are traces that reach the end*) -Goal - "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ -\ ==> EX NB. EX evs: woolam. \ -\ Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) : set evs"; +Goal "[| A ~= B; A ~= Server; B ~= Server |] \ +\ ==> EX NB. EX evs: woolam. \ +\ Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) : set evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS woolam.WL4 RS woolam.WL5) 2); @@ -35,7 +34,7 @@ (**** Inductive proofs about woolam ****) (*Nobody sends themselves messages*) -Goal "!!evs. evs : woolam ==> ALL A X. Says A A X ~: set evs"; +Goal "evs : woolam ==> ALL A X. Says A A X ~: set evs"; by (etac woolam.induct 1); by Auto_tac; qed_spec_mp "not_Says_to_self"; @@ -45,7 +44,7 @@ (** For reasoning about the encrypted portion of messages **) -Goal "!!evs. Says A' B X : set evs ==> X : analz (spies evs)"; +Goal "Says A' B X : set evs ==> X : analz (spies evs)"; by (etac (Says_imp_spies RS analz.Inj) 1); qed "WL4_analz_spies"; @@ -63,15 +62,13 @@ sends messages containing X! **) (*Spy never sees another agent's shared key! (unless it's bad at start)*) -Goal - "!!evs. evs : woolam ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; +Goal "evs : woolam ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; by (parts_induct_tac 1); by (Blast_tac 1); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; -Goal - "!!evs. evs : woolam ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; +Goal "evs : woolam ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; by Auto_tac; qed "Spy_analz_shrK"; Addsimps [Spy_analz_shrK]; @@ -86,10 +83,9 @@ (*** WL4 ***) (*If the encrypted message appears then it originated with Alice*) -Goal - "!!evs. [| Crypt (shrK A) (Nonce NB) : parts (spies evs); \ -\ A ~: bad; evs : woolam |] \ -\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs"; +Goal "[| Crypt (shrK A) (Nonce NB) : parts (spies evs); \ +\ A ~: bad; evs : woolam |] \ +\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs"; by (etac rev_mp 1); by (parts_induct_tac 1); by (ALLGOALS Blast_tac); @@ -98,11 +94,10 @@ (*Guarantee for Server: if it gets a message containing a certificate from Alice, then she originated that certificate. But we DO NOT know that B ever saw it: the Spy may have rerouted the message to the Server.*) -Goal - "!!evs. [| Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \ -\ : set evs; \ -\ A ~: bad; evs : woolam |] \ -\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs"; +Goal "[| Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \ +\ : set evs; \ +\ A ~: bad; evs : woolam |] \ +\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs"; by (blast_tac (claset() addSIs [NB_Crypt_imp_Alice_msg]) 1); qed "Server_trusts_WL4"; @@ -112,11 +107,10 @@ (*** WL5 ***) (*Server sent WL5 only if it received the right sort of message*) -Goal - "!!evs. [| Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs; \ -\ evs : woolam |] \ -\ ==> EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \ -\ : set evs"; +Goal "[| Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs; \ +\ evs : woolam |] \ +\ ==> EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \ +\ : set evs"; by (etac rev_mp 1); by (parts_induct_tac 1); by (ALLGOALS Blast_tac); @@ -125,10 +119,9 @@ AddDs [Server_sent_WL5]; (*If the encrypted message appears then it originated with the Server!*) -Goal - "!!evs. [| Crypt (shrK B) {|Agent A, NB|} : parts (spies evs); \ -\ B ~: bad; evs : woolam |] \ -\ ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs"; +Goal "[| Crypt (shrK B) {|Agent A, NB|} : parts (spies evs); \ +\ B ~: bad; evs : woolam |] \ +\ ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs"; by (etac rev_mp 1); by (parts_induct_tac 1); by (Blast_tac 1); @@ -138,18 +131,16 @@ the nonce using her key. This event can be no older than the nonce itself. But A may have sent the nonce to some other agent and it could have reached the Server via the Spy.*) -Goal - "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs; \ -\ A ~: bad; B ~: bad; evs : woolam |] \ -\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs"; +Goal "[| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs; \ +\ A ~: bad; B ~: bad; evs : woolam |] \ +\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs"; by (blast_tac (claset() addSDs [NB_Crypt_imp_Server_msg]) 1); qed "B_trusts_WL5"; (*B only issues challenges in response to WL1. Not used.*) -Goal - "!!evs. [| Says B A (Nonce NB) : set evs; B ~= Spy; evs : woolam |] \ -\ ==> EX A'. Says A' B (Agent A) : set evs"; +Goal "[| Says B A (Nonce NB) : set evs; B ~= Spy; evs : woolam |] \ +\ ==> EX A'. Says A' B (Agent A) : set evs"; by (etac rev_mp 1); by (parts_induct_tac 1); by (ALLGOALS Blast_tac); @@ -157,11 +148,10 @@ (**CANNOT be proved because A doesn't know where challenges come from... -Goal - "!!evs. [| A ~: bad; B ~= Spy; evs : woolam |] \ -\ ==> Crypt (shrK A) (Nonce NB) : parts (spies evs) & \ -\ Says B A (Nonce NB) : set evs \ -\ --> Says A B (Crypt (shrK A) (Nonce NB)) : set evs"; +Goal "[| A ~: bad; B ~= Spy; evs : woolam |] \ +\ ==> Crypt (shrK A) (Nonce NB) : parts (spies evs) & \ +\ Says B A (Nonce NB) : set evs \ +\ --> Says A B (Crypt (shrK A) (Nonce NB)) : set evs"; by (parts_induct_tac 1); by (Blast_tac 1); by Safe_tac; diff -r c4da11bb0592 -r c729d4c299c1 src/HOL/Auth/Yahalom.ML --- a/src/HOL/Auth/Yahalom.ML Thu Jul 02 17:27:35 1998 +0200 +++ b/src/HOL/Auth/Yahalom.ML Thu Jul 02 17:48:11 1998 +0200 @@ -18,10 +18,9 @@ (*A "possibility property": there are traces that reach the end*) -Goal - "!!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"; +Goal "[| 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 yahalom.YM4) 2); @@ -32,7 +31,7 @@ (**** Inductive proofs about yahalom ****) (*Nobody sends themselves messages*) -Goal "!!evs. evs: yahalom ==> ALL A X. Says A A X ~: set evs"; +Goal "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"; @@ -43,8 +42,8 @@ (** For reasoning about the encrypted portion of messages **) (*Lets us treat YM4 using a similar argument as for the Fake case.*) -Goal "!!evs. Says S A {|Crypt (shrK A) Y, X|} : set evs ==> \ -\ X : analz (spies evs)"; +Goal "Says S A {|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"; @@ -52,8 +51,8 @@ YM4_analz_spies RS (impOfSubs analz_subset_parts)); (*Relates to both YM4 and Oops*) -Goal "!!evs. Says S A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs ==> \ -\ K : parts (spies evs)"; +Goal "Says S A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs ==> \ +\ K : parts (spies evs)"; by (blast_tac (claset() addSEs partsEs addSDs [Says_imp_spies RS parts.Inj]) 1); qed "YM4_Key_parts_spies"; @@ -78,16 +77,14 @@ sends messages containing X! **) (*Spy never sees another agent's shared key! (unless it's bad at start)*) -Goal - "!!evs. evs : yahalom ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; +Goal "evs : yahalom ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); by (ALLGOALS Blast_tac); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; -Goal - "!!evs. evs : yahalom ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; +Goal "evs : yahalom ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); qed "Spy_analz_shrK"; Addsimps [Spy_analz_shrK]; @@ -97,8 +94,8 @@ (*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*) -Goal "!!evs. evs : yahalom ==> \ -\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; +Goal "evs : yahalom ==> \ +\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; by (parts_induct_tac 1); (*Fake*) by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); @@ -115,11 +112,10 @@ (*Describes the form of K when the Server sends this message. Useful for Oops as well as main secrecy property.*) -Goal - "!!evs. [| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \ -\ : set evs; \ -\ evs : yahalom |] \ -\ ==> K ~: range shrK"; +Goal "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \ +\ : set evs; \ +\ evs : yahalom |] \ +\ ==> K ~: range shrK"; by (etac rev_mp 1); by (etac yahalom.induct 1); by (ALLGOALS Asm_simp_tac); @@ -143,11 +139,10 @@ (** Session keys are not used to encrypt other session keys **) -Goal - "!!evs. evs : yahalom ==> \ +Goal "evs : yahalom ==> \ \ ALL K KK. KK <= Compl (range shrK) --> \ -\ (Key K : analz (Key``KK Un (spies evs))) = \ -\ (K : KK | Key K : analz (spies evs))"; +\ (Key K : analz (Key``KK Un (spies evs))) = \ +\ (K : KK | Key K : analz (spies evs))"; by (etac yahalom.induct 1); by analz_spies_tac; by (REPEAT_FIRST (resolve_tac [allI, impI])); @@ -158,22 +153,20 @@ by (spy_analz_tac 1); qed_spec_mp "analz_image_freshK"; -Goal - "!!evs. [| evs : yahalom; KAB ~: range shrK |] \ -\ ==> Key K : analz (insert (Key KAB) (spies evs)) = \ -\ (K = KAB | Key K : analz (spies evs))"; +Goal "[| evs : yahalom; 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"; (*** The Key K uniquely identifies the Server's message. **) -Goal - "!!evs. evs : yahalom ==> \ -\ EX A' B' na' nb' X'. ALL A B na nb X. \ -\ Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \ -\ : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'"; +Goal "evs : yahalom ==> \ +\ EX A' B' na' nb' X'. ALL A B na nb X. \ +\ Says Server A \ +\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, 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]))); by (ALLGOALS Clarify_tac); @@ -187,27 +180,25 @@ delrules [conjI] (*no split-up to 4 subgoals*)) 1); val lemma = result(); -Goal -"!!evs. [| Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} : set evs; \ -\ Says Server A' \ -\ {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} : set evs; \ -\ evs : yahalom |] \ -\ ==> A=A' & B=B' & na=na' & nb=nb'"; +Goal "[| Says Server A \ +\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} : set evs; \ +\ Says Server A' \ +\ {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} : set evs; \ +\ evs : yahalom |] \ +\ ==> A=A' & B=B' & na=na' & nb=nb'"; by (prove_unique_tac lemma 1); qed "unique_session_keys"; (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **) -Goal - "!!evs. [| A ~: bad; B ~: bad; evs : yahalom |] \ -\ ==> Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \ -\ Crypt (shrK B) {|Agent A, Key K|}|} \ -\ : set evs --> \ -\ Notes Spy {|na, nb, Key K|} ~: set evs --> \ -\ Key K ~: analz (spies evs)"; +Goal "[| A ~: bad; B ~: bad; evs : yahalom |] \ +\ ==> Says Server A \ +\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \ +\ Crypt (shrK B) {|Agent A, Key K|}|} \ +\ : set evs --> \ +\ Notes Spy {|na, nb, Key K|} ~: set evs --> \ +\ Key K ~: analz (spies evs)"; by (etac yahalom.induct 1); by analz_spies_tac; by (ALLGOALS @@ -226,14 +217,13 @@ (*Final version*) -Goal - "!!evs. [| Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \ -\ Crypt (shrK B) {|Agent A, Key K|}|} \ -\ : set evs; \ -\ Notes Spy {|na, nb, Key K|} ~: set evs; \ -\ A ~: bad; B ~: bad; evs : yahalom |] \ -\ ==> Key K ~: analz (spies evs)"; +Goal "[| Says Server A \ +\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \ +\ Crypt (shrK B) {|Agent A, Key K|}|} \ +\ : set evs; \ +\ Notes Spy {|na, nb, Key K|} ~: set evs; \ +\ A ~: bad; B ~: bad; evs : yahalom |] \ +\ ==> Key K ~: analz (spies evs)"; by (blast_tac (claset() addSEs [lemma]) 1); qed "Spy_not_see_encrypted_key"; @@ -241,24 +231,22 @@ (** Security Guarantee for A upon receiving YM3 **) (*If the encrypted message appears then it originated with the Server*) -Goal - "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (spies evs); \ -\ A ~: bad; evs : yahalom |] \ -\ ==> Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \ -\ Crypt (shrK B) {|Agent A, Key K|}|} \ -\ : set evs"; +Goal "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (spies evs); \ +\ A ~: bad; evs : yahalom |] \ +\ ==> Says Server A \ +\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \ +\ Crypt (shrK B) {|Agent A, Key K|}|} \ +\ : set evs"; by (etac rev_mp 1); by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); qed "A_trusts_YM3"; (*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*) -Goal - "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (spies evs); \ -\ Notes Spy {|na, nb, Key K|} ~: set evs; \ -\ A ~: bad; B ~: bad; evs : yahalom |] \ -\ ==> Key K ~: analz (spies evs)"; +Goal "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (spies evs); \ +\ Notes Spy {|na, nb, Key K|} ~: set evs; \ +\ A ~: bad; B ~: bad; evs : yahalom |] \ +\ ==> Key K ~: analz (spies evs)"; by (blast_tac (claset() addSDs [A_trusts_YM3, Spy_not_see_encrypted_key]) 1); qed "A_gets_good_key"; @@ -266,14 +254,13 @@ (*B knows, by the first part of A's message, that the Server distributed the key for A and B. But this part says nothing about nonces.*) -Goal - "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (spies evs); \ -\ B ~: bad; evs : yahalom |] \ -\ ==> EX NA NB. Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, \ -\ Nonce NA, Nonce NB|}, \ -\ Crypt (shrK B) {|Agent A, Key K|}|} \ -\ : set evs"; +Goal "[| Crypt (shrK B) {|Agent A, Key K|} : parts (spies evs); \ +\ B ~: bad; evs : yahalom |] \ +\ ==> EX NA NB. Says Server A \ +\ {|Crypt (shrK A) {|Agent B, Key K, \ +\ Nonce NA, Nonce NB|}, \ +\ Crypt (shrK B) {|Agent A, Key K|}|} \ +\ : set evs"; by (etac rev_mp 1); by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); @@ -285,15 +272,14 @@ the key quoting nonce NB. This part says nothing about agent names. Secrecy of NB is crucial. Note that Nonce NB ~: analz (spies evs) must be the FIRST antecedent of the induction formula.*) -Goal - "!!evs. evs : yahalom \ -\ ==> Nonce NB ~: analz (spies evs) --> \ -\ Crypt K (Nonce NB) : parts (spies evs) --> \ -\ (EX A B NA. Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, \ -\ Nonce NA, Nonce NB|}, \ -\ Crypt (shrK B) {|Agent A, Key K|}|} \ -\ : set evs)"; +Goal "evs : yahalom \ +\ ==> Nonce NB ~: analz (spies evs) --> \ +\ Crypt K (Nonce NB) : parts (spies evs) --> \ +\ (EX A B NA. Says Server A \ +\ {|Crypt (shrK A) {|Agent B, Key K, \ +\ Nonce NA, Nonce NB|}, \ +\ Crypt (shrK B) {|Agent A, Key K|}|} \ +\ : set evs)"; by (parts_induct_tac 1); by (ALLGOALS Clarify_tac); (*YM3 & Fake*) @@ -313,17 +299,17 @@ (** Lemmas about the predicate KeyWithNonce **) Goalw [KeyWithNonce_def] - "!!evs. Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \ -\ : set evs ==> KeyWithNonce K NB evs"; + "Says Server A \ +\ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \ +\ : set evs ==> KeyWithNonce K NB evs"; by (Blast_tac 1); qed "KeyWithNonceI"; Goalw [KeyWithNonce_def] "KeyWithNonce K NB (Says S A X # evs) = \ -\ (Server = S & \ -\ (EX B n X'. X = {|Crypt (shrK A) {|Agent B, Key K, n, Nonce NB|}, X'|}) \ -\ | KeyWithNonce K NB evs)"; +\ (Server = S & \ +\ (EX B n X'. X = {|Crypt (shrK A) {|Agent B, Key K, n, Nonce NB|}, X'|}) \ +\ | KeyWithNonce K NB evs)"; by (Simp_tac 1); by (Blast_tac 1); qed "KeyWithNonce_Says"; @@ -338,18 +324,18 @@ (*A fresh key cannot be associated with any nonce (with respect to a given trace). *) Goalw [KeyWithNonce_def] - "!!evs. Key K ~: used evs ==> ~ KeyWithNonce K NB evs"; + "Key K ~: used evs ==> ~ KeyWithNonce K NB evs"; by (blast_tac (claset() addSEs spies_partsEs) 1); qed "fresh_not_KeyWithNonce"; (*The Server message associates K with NB' and therefore not with any other nonce NB.*) Goalw [KeyWithNonce_def] - "!!evs. [| Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|} \ -\ : set evs; \ -\ NB ~= NB'; evs : yahalom |] \ -\ ==> ~ KeyWithNonce K NB evs"; + "[| Says Server A \ +\ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|} \ +\ : set evs; \ +\ NB ~= NB'; evs : yahalom |] \ +\ ==> ~ KeyWithNonce K NB evs"; by (blast_tac (claset() addDs [unique_session_keys]) 1); qed "Says_Server_KeyWithNonce"; @@ -361,24 +347,22 @@ (*As with analz_image_freshK, we take some pains to express the property as a logical equivalence so that the simplifier can apply it.*) -Goal - "!!evs. P --> (X : analz (G Un H)) --> (X : analz H) ==> \ -\ P --> (X : analz (G Un H)) = (X : analz H)"; +Goal "P --> (X : analz (G Un H)) --> (X : analz H) ==> \ +\ P --> (X : analz (G Un H)) = (X : analz H)"; by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1); val Nonce_secrecy_lemma = result(); -Goal - "!!evs. evs : yahalom ==> \ -\ (ALL KK. KK <= Compl (range shrK) --> \ -\ (ALL K: KK. ~ KeyWithNonce K NB evs) --> \ -\ (Nonce NB : analz (Key``KK Un (spies evs))) = \ -\ (Nonce NB : analz (spies evs)))"; +Goal "evs : yahalom ==> \ +\ (ALL KK. KK <= Compl (range shrK) --> \ +\ (ALL K: KK. ~ KeyWithNonce K NB evs) --> \ +\ (Nonce NB : analz (Key``KK Un (spies evs))) = \ +\ (Nonce NB : analz (spies evs)))"; by (etac yahalom.induct 1); by analz_spies_tac; by (REPEAT_FIRST (resolve_tac [impI RS allI])); by (REPEAT_FIRST (rtac Nonce_secrecy_lemma)); (*For Oops, simplification proves NBa~=NB. By Says_Server_KeyWithNonce, - we get (~ KeyWithNonce K NB evsa); then simplification can apply the + we get (~ KeyWithNonce K NB evs); then simplification can apply the induction hypothesis with KK = {K}.*) by (ALLGOALS (*4 seconds*) (asm_simp_tac @@ -402,13 +386,12 @@ (*Version required below: if NB can be decrypted using a session key then it was distributed with that key. The more general form above is required for the induction to carry through.*) -Goal - "!!evs. [| Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|} \ -\ : set evs; \ -\ NB ~= NB'; KAB ~: range shrK; evs : yahalom |] \ -\ ==> (Nonce NB : analz (insert (Key KAB) (spies evs))) = \ -\ (Nonce NB : analz (spies evs))"; +Goal "[| Says Server A \ +\ {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|} \ +\ : set evs; \ +\ NB ~= NB'; KAB ~: range shrK; evs : yahalom |] \ +\ ==> (Nonce NB : analz (insert (Key KAB) (spies evs))) = \ +\ (Nonce NB : analz (spies evs))"; by (asm_simp_tac (analz_image_freshK_ss addsimps [Nonce_secrecy, Says_Server_KeyWithNonce]) 1); qed "single_Nonce_secrecy"; @@ -416,11 +399,10 @@ (*** The Nonce NB uniquely identifies B's message. ***) -Goal - "!!evs. evs : yahalom ==> \ -\ EX NA' A' B'. ALL NA A B. \ -\ Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(spies evs) \ -\ --> B ~: bad --> NA = NA' & A = A' & B = B'"; +Goal "evs : yahalom ==> \ +\EX NA' A' B'. ALL NA A B. \ +\ Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(spies evs) \ +\ --> B ~: bad --> NA = NA' & A = A' & B = B'"; by (parts_induct_tac 1); (*Fake*) by (REPEAT (etac (exI RSN (2,exE)) 1) (*stripping EXs makes proof faster*) @@ -432,24 +414,22 @@ by (blast_tac (claset() addSEs spies_partsEs) 1); val lemma = result(); -Goal - "!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (spies evs); \ -\ Crypt (shrK B') {|Agent A', Nonce NA', nb|} : parts (spies evs); \ -\ evs : yahalom; B ~: bad; B' ~: bad |] \ -\ ==> NA' = NA & A' = A & B' = B"; +Goal "[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (spies evs); \ +\ Crypt (shrK B') {|Agent A', Nonce NA', nb|} : parts (spies evs); \ +\ evs : yahalom; B ~: bad; B' ~: bad |] \ +\ ==> NA' = NA & A' = A & B' = B"; by (prove_unique_tac lemma 1); qed "unique_NB"; (*Variant useful for proving secrecy of NB: the Says... form allows not_bad_tac to remove the assumption B' ~: bad.*) -Goal - "!!evs.[| Says C D {|X, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \ -\ : set evs; B ~: bad; \ -\ Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|} \ -\ : set evs; \ -\ nb ~: analz (spies evs); evs : yahalom |] \ -\ ==> NA' = NA & A' = A & B' = B"; +Goal "[| Says C D {|X, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \ +\ : set evs; B ~: bad; \ +\ Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|} \ +\ : set evs; \ +\ nb ~: analz (spies evs); evs : yahalom |] \ +\ ==> NA' = NA & A' = A & B' = B"; by (not_bad_tac "B'" 1); by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj] addSEs [MPair_parts] @@ -459,11 +439,10 @@ (** A nonce value is never used both as NA and as NB **) -Goal - "!!evs. evs : yahalom \ +Goal "evs : yahalom \ \ ==> Nonce NB ~: analz (spies evs) --> \ -\ Crypt (shrK B') {|Agent A', Nonce NB, nb'|} : parts(spies evs) --> \ -\ Crypt (shrK B) {|Agent A, na, Nonce NB|} ~: parts(spies evs)"; +\ Crypt (shrK B') {|Agent A', Nonce NB, nb'|} : parts(spies evs) --> \ +\ Crypt (shrK B) {|Agent A, na, Nonce NB|} ~: parts(spies evs)"; by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj] @@ -475,13 +454,12 @@ standard (result() RS mp RSN (2,rev_mp)); (*The Server sends YM3 only in response to YM2.*) -Goal - "!!evs. [| Says Server A \ -\ {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set evs; \ -\ evs : yahalom |] \ -\ ==> EX B'. Says B' Server \ -\ {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \ -\ : set evs"; +Goal "[| Says Server A \ +\ {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set evs; \ +\ evs : yahalom |] \ +\ ==> EX B'. Says B' Server \ +\ {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \ +\ : set evs"; by (etac rev_mp 1); by (etac yahalom.induct 1); by (ALLGOALS Asm_simp_tac); @@ -490,13 +468,12 @@ (*A vital theorem for B, that nonce NB remains secure from the Spy.*) -Goal - "!!evs. [| A ~: bad; B ~: bad; evs : yahalom |] \ +Goal "[| A ~: bad; B ~: bad; evs : yahalom |] \ \ ==> Says B Server \ -\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \ -\ : set evs --> \ -\ (ALL k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs) --> \ -\ Nonce NB ~: analz (spies evs)"; +\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \ +\ : set evs --> \ +\ (ALL k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs) --> \ +\ Nonce NB ~: analz (spies evs)"; by (etac yahalom.induct 1); by analz_spies_tac; by (ALLGOALS @@ -549,19 +526,18 @@ assumption must quantify over ALL POSSIBLE keys instead of our particular K. If this run is broken and the spy substitutes a certificate containing an old key, B has no means of telling.*) -Goal - "!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Key K|}, \ -\ Crypt K (Nonce NB)|} : set evs; \ -\ Says B Server \ -\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \ -\ : set evs; \ -\ ALL k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs; \ -\ A ~: bad; B ~: bad; evs : yahalom |] \ -\ ==> Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, \ -\ Nonce NA, Nonce NB|}, \ -\ Crypt (shrK B) {|Agent A, Key K|}|} \ -\ : set evs"; +Goal "[| Says A' B {|Crypt (shrK B) {|Agent A, Key K|}, \ +\ Crypt K (Nonce NB)|} : set evs; \ +\ Says B Server \ +\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \ +\ : set evs; \ +\ ALL k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs; \ +\ A ~: bad; B ~: bad; evs : yahalom |] \ +\ ==> Says Server A \ +\ {|Crypt (shrK A) {|Agent B, Key K, \ +\ Nonce NA, Nonce NB|}, \ +\ Crypt (shrK B) {|Agent A, Key K|}|} \ +\ : set evs"; by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1 THEN dtac B_trusts_YM4_shrK 1); @@ -574,15 +550,14 @@ (*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*) -Goal - "!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Key K|}, \ -\ Crypt K (Nonce NB)|} : set evs; \ -\ Says B Server \ -\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \ -\ : set evs; \ -\ ALL k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs; \ -\ A ~: bad; B ~: bad; evs : yahalom |] \ -\ ==> Key K ~: analz (spies evs)"; +Goal "[| Says A' B {|Crypt (shrK B) {|Agent A, Key K|}, \ +\ Crypt K (Nonce NB)|} : set evs; \ +\ Says B Server \ +\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \ +\ : set evs; \ +\ ALL k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs; \ +\ A ~: bad; B ~: bad; evs : yahalom |] \ +\ ==> Key K ~: analz (spies evs)"; by (blast_tac (claset() addSDs [B_trusts_YM4, Spy_not_see_encrypted_key]) 1); qed "B_gets_good_key"; @@ -590,24 +565,22 @@ (*** Authenticating B to A ***) (*The encryption in message YM2 tells us it cannot be faked.*) -Goal - "!!evs. evs : yahalom \ +Goal "evs : yahalom \ \ ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (spies evs) --> \ -\ B ~: bad --> \ -\ Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \ -\ : set evs"; +\ B ~: bad --> \ +\ Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \ +\ : set evs"; by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp); (*If the server sends YM3 then B sent YM2*) -Goal - "!!evs. evs : yahalom \ +Goal "evs : yahalom \ \ ==> Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \ -\ : set evs --> \ -\ B ~: bad --> \ -\ Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \ -\ : set evs"; +\ : set evs --> \ +\ B ~: bad --> \ +\ Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \ +\ : set evs"; by (etac yahalom.induct 1); by (ALLGOALS Asm_simp_tac); (*YM4*) @@ -618,12 +591,11 @@ val lemma = result() RSN (2, rev_mp) RS mp |> standard; (*If A receives YM3 then B has used nonce NA (and therefore is alive)*) -Goal - "!!evs. [| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \ -\ : set evs; \ -\ A ~: bad; B ~: bad; evs : yahalom |] \ -\ ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \ -\ : set evs"; +Goal "[| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \ +\ : set evs; \ +\ A ~: bad; B ~: bad; evs : yahalom |] \ +\==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \ +\ : set evs"; by (blast_tac (claset() addSDs [A_trusts_YM3, lemma] addEs spies_partsEs) 1); qed "YM3_auth_B_to_A"; @@ -634,13 +606,12 @@ (*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 - "!!evs. evs : yahalom \ -\ ==> Key K ~: analz (spies evs) --> \ -\ Crypt K (Nonce NB) : parts (spies evs) --> \ -\ Crypt (shrK B) {|Agent A, Key K|} : parts (spies evs) --> \ -\ B ~: bad --> \ -\ (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)"; +Goal "evs : yahalom \ +\ ==> Key K ~: analz (spies evs) --> \ +\ Crypt K (Nonce NB) : parts (spies evs) --> \ +\ Crypt (shrK B) {|Agent A, Key K|} : parts (spies evs) --> \ +\ B ~: bad --> \ +\ (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)"; by (parts_induct_tac 1); (*Fake*) by (Fake_parts_insert_tac 1); @@ -659,15 +630,14 @@ (*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 - "!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Key K|}, \ -\ Crypt K (Nonce NB)|} : set evs; \ -\ Says B Server \ -\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \ -\ : set evs; \ -\ (ALL NA k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs); \ -\ A ~: bad; B ~: bad; evs : yahalom |] \ -\ ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs"; +Goal "[| Says A' B {|Crypt (shrK B) {|Agent A, Key K|}, \ +\ Crypt K (Nonce NB)|} : set evs; \ +\ Says B Server \ +\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \ +\ : set evs; \ +\ (ALL NA k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs); \ +\ A ~: bad; B ~: bad; evs : yahalom |] \ +\ ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs"; by (forward_tac [B_trusts_YM4] 1); by (REPEAT_FIRST (eresolve_tac [asm_rl, spec])); by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1); diff -r c4da11bb0592 -r c729d4c299c1 src/HOL/Auth/Yahalom2.ML --- a/src/HOL/Auth/Yahalom2.ML Thu Jul 02 17:27:35 1998 +0200 +++ b/src/HOL/Auth/Yahalom2.ML Thu Jul 02 17:48:11 1998 +0200 @@ -23,10 +23,9 @@ (*A "possibility property": there are traces that reach the end*) -Goal - "!!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"; +Goal "[| 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 yahalom.YM4) 2); @@ -37,7 +36,7 @@ (**** Inductive proofs about yahalom ****) (*Nobody sends themselves messages*) -Goal "!!evs. evs: yahalom ==> ALL A X. Says A A X ~: set evs"; +Goal "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,8 +47,8 @@ (** For reasoning about the encrypted portion of messages **) (*Lets us treat YM4 using a similar argument as for the Fake case.*) -Goal "!!evs. Says S A {|NB, Crypt (shrK A) Y, X|} : set evs ==> \ -\ X : analz (spies evs)"; +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"; @@ -57,8 +56,8 @@ YM4_analz_spies RS (impOfSubs analz_subset_parts)); (*Relates to both YM4 and Oops*) -Goal "!!evs. Says S A {|NB, Crypt (shrK A) {|B,K,NA|}, X|} : set evs ==> \ -\ K : parts (spies evs)"; +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"; @@ -82,15 +81,13 @@ sends messages containing X! **) (*Spy never sees another agent's shared key! (unless it's bad at start)*) -Goal - "!!evs. evs : yahalom ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; +Goal "evs : yahalom ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; by (parts_induct_tac 1); by (ALLGOALS Blast_tac); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; -Goal - "!!evs. evs : yahalom ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; +Goal "evs : yahalom ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; by Auto_tac; qed "Spy_analz_shrK"; Addsimps [Spy_analz_shrK]; @@ -100,8 +97,8 @@ (*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*) -Goal "!!evs. evs : yahalom ==> \ -\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; +Goal "evs : yahalom ==> \ +\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; by (parts_induct_tac 1); (*YM4: Key K is not fresh!*) by (Blast_tac 3); @@ -119,11 +116,10 @@ (*Describes the form of K when the Server sends this message. Useful for Oops as well as main secrecy property.*) -Goal - "!!evs. [| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|} \ -\ : set evs; \ -\ evs : yahalom |] \ -\ ==> K ~: range shrK & A ~= B"; +Goal "[| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|} \ +\ : set evs; \ +\ evs : yahalom |] \ +\ ==> K ~: range shrK & A ~= B"; by (etac rev_mp 1); by (etac yahalom.induct 1); by (ALLGOALS Asm_simp_tac); @@ -150,11 +146,10 @@ (** Session keys are not used to encrypt other session keys **) -Goal - "!!evs. evs : yahalom ==> \ +Goal "evs : yahalom ==> \ \ ALL K KK. KK <= Compl (range shrK) --> \ -\ (Key K : analz (Key``KK Un (spies evs))) = \ -\ (K : KK | Key K : analz (spies evs))"; +\ (Key K : analz (Key``KK Un (spies evs))) = \ +\ (K : KK | Key K : analz (spies evs))"; by (etac yahalom.induct 1); by analz_spies_tac; by (REPEAT_FIRST (resolve_tac [allI, impI])); @@ -164,22 +159,20 @@ by (spy_analz_tac 1); qed_spec_mp "analz_image_freshK"; -Goal - "!!evs. [| evs : yahalom; KAB ~: range shrK |] ==> \ -\ Key K : analz (insert (Key KAB) (spies evs)) = \ -\ (K = KAB | Key K : analz (spies evs))"; +Goal "[| evs : yahalom; 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"; (*** The Key K uniquely identifies the Server's message. **) -Goal - "!!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'"; +Goal "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]))); by (Clarify_tac 1); @@ -191,28 +184,26 @@ addss (simpset() addsimps [parts_insertI])) 1); val lemma = result(); -Goal -"!!evs. [| Says Server A \ -\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} : set evs; \ -\ Says Server A' \ -\ {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|} : set evs; \ -\ evs : yahalom |] \ -\ ==> A=A' & B=B' & na=na' & nb=nb'"; +Goal "[| Says Server A \ +\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} : set evs; \ +\ Says Server A' \ +\ {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|} : set evs; \ +\ evs : yahalom |] \ +\ ==> A=A' & B=B' & na=na' & nb=nb'"; by (prove_unique_tac lemma 1); qed "unique_session_keys"; (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **) -Goal - "!!evs. [| A ~: bad; B ~: bad; A ~= B; \ -\ evs : yahalom |] \ -\ ==> Says Server A \ -\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \ -\ 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)"; +Goal "[| A ~: bad; B ~: bad; A ~= B; \ +\ evs : yahalom |] \ +\ ==> Says Server A \ +\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \ +\ 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)"; by (etac yahalom.induct 1); by analz_spies_tac; by (ALLGOALS @@ -229,14 +220,13 @@ (*Final version*) -Goal - "!!evs. [| Says Server A \ -\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \ -\ Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \ -\ : set evs; \ -\ Notes Spy {|na, nb, Key K|} ~: set evs; \ -\ A ~: bad; B ~: bad; evs : yahalom |] \ -\ ==> Key K ~: analz (spies evs)"; +Goal "[| Says Server A \ +\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \ +\ Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \ +\ : set evs; \ +\ Notes Spy {|na, nb, Key K|} ~: set evs; \ +\ A ~: bad; B ~: bad; evs : yahalom |] \ +\ ==> Key K ~: analz (spies 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"; @@ -246,25 +236,23 @@ (*If the encrypted message appears then it originated with the Server. May now apply Spy_not_see_encrypted_key, subject to its conditions.*) -Goal - "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na|} \ -\ : parts (spies evs); \ -\ A ~: bad; evs : yahalom |] \ -\ ==> EX nb. Says Server A \ -\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \ -\ Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \ -\ : set evs"; +Goal "[| Crypt (shrK A) {|Agent B, Key K, na|} \ +\ : parts (spies evs); \ +\ A ~: bad; evs : yahalom |] \ +\ ==> EX nb. Says Server A \ +\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \ +\ Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \ +\ : set evs"; by (etac rev_mp 1); by (parts_induct_tac 1); by (ALLGOALS Blast_tac); qed "A_trusts_YM3"; (*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*) -Goal - "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na|} : parts (spies evs); \ -\ ALL nb. Notes Spy {|na, nb, Key K|} ~: set evs; \ -\ A ~: bad; B ~: bad; evs : yahalom |] \ -\ ==> Key K ~: analz (spies evs)"; +Goal "[| Crypt (shrK A) {|Agent B, Key K, na|} : parts (spies evs); \ +\ ALL nb. Notes Spy {|na, nb, Key K|} ~: set evs; \ +\ A ~: bad; B ~: bad; evs : yahalom |] \ +\ ==> Key K ~: analz (spies evs)"; by (blast_tac (claset() addSDs [A_trusts_YM3, Spy_not_see_encrypted_key]) 1); qed "A_gets_good_key"; @@ -273,15 +261,14 @@ (*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 - "!!evs. [| Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|} \ -\ : parts (spies evs); \ -\ B ~: bad; evs : yahalom |] \ +Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|} \ +\ : parts (spies evs); \ +\ B ~: bad; evs : yahalom |] \ \ ==> EX NA. Says Server A \ -\ {|Nonce NB, \ -\ Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, \ -\ Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|} \ -\ : set evs"; +\ {|Nonce NB, \ +\ Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, \ +\ Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|} \ +\ : set evs"; by (etac rev_mp 1); by (parts_induct_tac 1); by (ALLGOALS Blast_tac); @@ -293,28 +280,26 @@ (*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 - "!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \ -\ X|} \ -\ : set evs; \ -\ A ~: bad; B ~: bad; evs : yahalom |] \ +Goal "[| Says A' B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \ +\ X|} \ +\ : set evs; \ +\ A ~: bad; B ~: bad; evs : yahalom |] \ \ ==> EX NA. Says Server A \ -\ {|Nonce NB, \ -\ Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, \ -\ Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|} \ -\ : set evs"; +\ {|Nonce NB, \ +\ Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, \ +\ Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|} \ +\ : set evs"; by (blast_tac (claset() addSDs [B_trusts_YM4_shrK]) 1); qed "B_trusts_YM4"; (*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*) -Goal - "!!evs. [| Says A' 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)"; +Goal "[| Says A' 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)"; by (blast_tac (claset() addSDs [B_trusts_YM4, Spy_not_see_encrypted_key]) 1); qed "B_gets_good_key"; @@ -323,12 +308,11 @@ (*** Authenticating B to A ***) (*The encryption in message YM2 tells us it cannot be faked.*) -Goal - "!!evs. [| Crypt (shrK B) {|Agent A, Nonce NA|} : parts (spies evs); \ -\ B ~: bad; evs : yahalom \ -\ |] ==> EX NB. Says B Server {|Agent B, Nonce NB, \ -\ Crypt (shrK B) {|Agent A, Nonce NA|}|} \ -\ : set evs"; +Goal "[| Crypt (shrK B) {|Agent A, Nonce NA|} : parts (spies evs); \ +\ B ~: bad; evs : yahalom \ +\ |] ==> EX NB. Says B Server {|Agent B, Nonce NB, \ +\ Crypt (shrK B) {|Agent A, Nonce NA|}|} \ +\ : set evs"; by (etac rev_mp 1); by (etac rev_mp 1); by (parts_induct_tac 1); @@ -337,14 +321,13 @@ (*If the server sends YM3 then B sent YM2, perhaps with a different NB*) -Goal - "!!evs. [| Says Server A \ -\ {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \ -\ : set evs; \ -\ B ~: bad; evs : yahalom \ -\ |] ==> EX nb'. Says B Server {|Agent B, nb', \ -\ Crypt (shrK B) {|Agent A, Nonce NA|}|} \ -\ : set evs"; +Goal "[| Says Server A \ +\ {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \ +\ : set evs; \ +\ B ~: bad; evs : yahalom \ +\ |] ==> EX nb'. Says B Server {|Agent B, nb', \ +\ Crypt (shrK B) {|Agent A, Nonce NA|}|} \ +\ : set evs"; by (etac rev_mp 1); by (etac rev_mp 1); by (etac yahalom.induct 1); @@ -356,13 +339,12 @@ val lemma = result(); (*If A receives YM3 then B has used nonce NA (and therefore is alive)*) -Goal - "!!evs. [| Says S A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \ -\ : set evs; \ -\ A ~: bad; B ~: bad; evs : yahalom |] \ -\ ==> EX nb'. Says B Server \ -\ {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} \ -\ : set evs"; +Goal "[| Says S A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \ +\ : set evs; \ +\ A ~: bad; B ~: bad; evs : yahalom |] \ +\==> EX nb'. Says B Server \ +\ {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} \ +\ : set evs"; by (blast_tac (claset() addSDs [A_trusts_YM3, lemma]) 1); qed "YM3_auth_B_to_A"; @@ -373,14 +355,13 @@ 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 the FIRST antecedent of the induction formula.*) -Goal - "!!evs. evs : yahalom \ -\ ==> Key K ~: analz (spies evs) --> \ -\ Crypt K (Nonce NB) : parts (spies evs) --> \ -\ Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|} \ -\ : parts (spies evs) --> \ -\ B ~: bad --> \ -\ (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)"; +Goal "evs : yahalom \ +\ ==> Key K ~: analz (spies evs) --> \ +\ Crypt K (Nonce NB) : parts (spies evs) --> \ +\ Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|} \ +\ : parts (spies evs) --> \ +\ B ~: bad --> \ +\ (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)"; by (parts_induct_tac 1); (*Fake*) by (Blast_tac 1); @@ -398,12 +379,11 @@ (*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 - "!!evs. [| Says A' 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"; +Goal "[| Says A' 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 (blast_tac (claset() addIs [Auth_A_to_B_lemma]) 1); by (blast_tac (claset() addDs [Spy_not_see_encrypted_key,