--- 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);
--- 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);
--- 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);
--- 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);
--- 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*)
--- 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; \
--- 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";
--- 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";
--- 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);
--- 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";
--- 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);
--- 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";
--- 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";
--- 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;
--- 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);
--- 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,