--- a/src/HOL/Auth/Event.ML Wed Jun 24 10:33:42 1998 +0200
+++ b/src/HOL/Auth/Event.ML Wed Jun 24 11:24:52 1998 +0200
@@ -22,7 +22,7 @@
read_instantiate_sg (sign_of thy) [("H", "spies evs")]);
-goal thy
+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)))";
@@ -30,34 +30,34 @@
by Auto_tac;
qed "expand_event_case";
-goal thy "spies (Says A B X # evs) = insert X (spies evs)";
+Goal "spies (Says A B X # evs) = insert X (spies evs)";
by (Simp_tac 1);
qed "spies_Says";
(*The point of letting the Spy see "bad" agents' notes is to prevent
redundant case-splits on whether A=Spy and whether A:bad*)
-goal thy "spies (Notes A X # evs) = \
+Goal "spies (Notes A X # evs) = \
\ (if A:bad then insert X (spies evs) else spies evs)";
by (Simp_tac 1);
qed "spies_Notes";
-goal thy "spies evs <= spies (Says A B X # evs)";
+Goal "spies evs <= spies (Says A B X # evs)";
by (simp_tac (simpset() addsimps [subset_insertI]) 1);
qed "spies_subset_spies_Says";
-goal thy "spies evs <= spies (Notes A X # evs)";
+Goal "spies evs <= spies (Notes A X # evs)";
by (Simp_tac 1);
by (Fast_tac 1);
qed "spies_subset_spies_Notes";
(*Spy sees all traffic*)
-goal thy "Says A B X : set evs --> X : spies evs";
+Goal "Says A B X : set evs --> X : spies evs";
by (induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
qed_spec_mp "Says_imp_spies";
(*Spy sees Notes of bad agents*)
-goal thy "Notes A X : set evs --> A: bad --> X : spies evs";
+Goal "Notes A X : set evs --> A: bad --> X : spies evs";
by (induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
qed_spec_mp "Notes_imp_spies";
@@ -74,7 +74,7 @@
(*** Fresh nonces ***)
-goal thy "parts (spies evs) <= used evs";
+Goal "parts (spies evs) <= used evs";
by (induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac
(simpset() addsimps [parts_insert_spies]
@@ -85,7 +85,7 @@
bind_thm ("usedI", impOfSubs parts_spies_subset_used);
AddIs [usedI];
-goal thy "parts (initState B) <= used evs";
+Goal "parts (initState B) <= used evs";
by (induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac
(simpset() addsimps [parts_insert_spies]
@@ -93,17 +93,17 @@
by (ALLGOALS Blast_tac);
bind_thm ("initState_into_used", impOfSubs (result()));
-goal thy "used (Says A B X # evs) = parts{X} Un used evs";
+Goal "used (Says A B X # evs) = parts{X} Un used evs";
by (Simp_tac 1);
qed "used_Says";
Addsimps [used_Says];
-goal thy "used (Notes A X # evs) = parts{X} Un used evs";
+Goal "used (Notes A X # evs) = parts{X} Un used evs";
by (Simp_tac 1);
qed "used_Notes";
Addsimps [used_Notes];
-goal thy "used [] <= used evs";
+Goal "used [] <= used evs";
by (Simp_tac 1);
by (blast_tac (claset() addIs [initState_into_used]) 1);
qed "used_nil_subset";
@@ -113,7 +113,7 @@
(*currently unused*)
-goal thy "used evs <= used (evs@evs')";
+Goal "used evs <= used (evs@evs')";
by (induct_tac "evs" 1);
by (simp_tac (simpset() addsimps [used_nil_subset]) 1);
by (induct_tac "a" 1);
--- a/src/HOL/Auth/Kerberos_BAN.ML Wed Jun 24 10:33:42 1998 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.ML Wed Jun 24 11:24:52 1998 +0200
@@ -33,7 +33,7 @@
(*A "possibility property": there are traces that reach the end.*)
-goal thy
+Goal
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX Timestamp K. EX evs: kerberos_ban. \
\ Says B A (Crypt K (Number Timestamp)) \
@@ -52,7 +52,7 @@
(**** Inductive proofs about kerberos_ban ****)
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : kerberos_ban ==> ALL A X. Says A A X ~: set evs";
+Goal "!!evs. 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,12 +61,12 @@
(*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*)
-goal thy "!!evs. Says S A (Crypt KA {|Timestamp, B, K, X|}) : set evs \
+Goal "!!evs. 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 thy
+Goal
"!!evs. Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) : set evs \
\ ==> K : parts (spies evs)";
by (Blast_tac 1);
@@ -81,7 +81,7 @@
(*Spy never sees another agent's shared key! (unless it's bad at start)*)
-goal thy
+Goal
"!!evs. evs : kerberos_ban ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
by (ALLGOALS Blast_tac);
@@ -89,13 +89,13 @@
Addsimps [Spy_see_shrK];
-goal thy
+Goal
"!!evs. evs : kerberos_ban ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
by Auto_tac;
qed "Spy_analz_shrK";
Addsimps [Spy_analz_shrK];
-goal thy "!!A. [| Key (shrK A) : parts (spies evs); \
+Goal "!!A. [| 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,7 +105,7 @@
(*Nobody can have used non-existent keys!*)
-goal thy "!!evs. evs : kerberos_ban ==> \
+Goal "!!evs. evs : kerberos_ban ==> \
\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*Fake*)
@@ -124,7 +124,7 @@
(** Lemmas concerning the form of items passed in messages **)
(*Describes the form of K, X and K' when the Server sends this message.*)
-goal thy
+Goal
"!!evs. [| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|}) \
\ : set evs; evs : kerberos_ban |] \
\ ==> K ~: range shrK & \
@@ -141,7 +141,7 @@
This shows implicitly the FRESHNESS OF THE SESSION KEY to A
*)
-goal thy
+Goal
"!!evs. [| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} \
\ : parts (spies evs); \
\ A ~: bad; evs : kerberos_ban |] \
@@ -155,7 +155,7 @@
(*If the TICKET appears then it originated with the Server*)
(*FRESHNESS OF THE SESSION KEY to B*)
-goal thy
+Goal
"!!evs. [| Crypt (shrK B) {|Number Ts, Agent A, Key K|} : parts (spies evs); \
\ B ~: bad; evs : kerberos_ban |] \
\ ==> Says Server A \
@@ -171,7 +171,7 @@
(*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 thy
+Goal
"!!evs. [| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
\ : set evs; \
\ evs : kerberos_ban |] \
@@ -206,7 +206,7 @@
(** Session keys are not used to encrypt other session keys **)
-goal thy
+Goal
"!!evs. evs : kerberos_ban ==> \
\ ALL K KK. KK <= Compl (range shrK) --> \
\ (Key K : analz (Key``KK Un (spies evs))) = \
@@ -222,7 +222,7 @@
qed_spec_mp "analz_image_freshK";
-goal thy
+Goal
"!!evs. [| evs : kerberos_ban; KAB ~: range shrK |] ==> \
\ Key K : analz (insert (Key KAB) (spies evs)) = \
\ (K = KAB | Key K : analz (spies evs))";
@@ -232,7 +232,7 @@
(** The session key K uniquely identifies the message **)
-goal thy
+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|}) \
@@ -248,7 +248,7 @@
val lemma = result();
(*In messages of this form, the session key uniquely identifies the rest*)
-goal thy
+Goal
"!!evs. [| Says Server A \
\ (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) : set evs; \
\ Says Server A' \
@@ -262,7 +262,7 @@
if the spy could see it!
**)
-goal thy
+Goal
"!!evs. [| A ~: bad; B ~: bad; evs : kerberos_ban |] \
\ ==> Says Server A \
\ (Crypt (shrK A) {|Number Ts, Agent B, Key K, \
@@ -294,7 +294,7 @@
Spy does not see the keys sent in msg Kb2
as long as they have NOT EXPIRED
**)
-goal thy
+Goal
"!!evs. [| Says Server A \
\ (Crypt K' {|Number T, Agent B, Key K, X|}) : set evs; \
\ ~ Expired T evs; \
@@ -312,7 +312,7 @@
(** CONFIDENTIALITY for ALICE: **)
(** Also A_trusts_K_by_Kb2 RS Confidentiality_S **)
-goal thy
+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 \
@@ -323,7 +323,7 @@
(** CONFIDENTIALITY for BOB: **)
(** Also B_trusts_K_by_Kb3 RS Confidentiality_S **)
-goal thy
+Goal
"!!evs. [| Crypt (shrK B) {|Number Tk, Agent A, Key K|} \
\ : parts (spies evs); \
\ ~ Expired Tk evs; \
@@ -334,7 +334,7 @@
qed "Confidentiality_B";
-goal thy
+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|}) \
@@ -367,7 +367,7 @@
(*AUTHENTICATION OF B TO A*)
-goal thy
+Goal
"!!evs. [| Crypt K (Number Ta) : parts (spies evs); \
\ Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} \
\ : parts (spies evs); \
@@ -380,7 +380,7 @@
qed "Authentication_B";
-goal thy
+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|}) \
@@ -404,7 +404,7 @@
(*AUTHENTICATION OF A TO B*)
-goal thy
+Goal
"!!evs. [| Crypt K {|Agent A, Number Ta|} : parts (spies evs); \
\ Crypt (shrK B) {|Number Ts, Agent A, Key K|} \
\ : parts (spies evs); \
--- a/src/HOL/Auth/Message.ML Wed Jun 24 10:33:42 1998 +0200
+++ b/src/HOL/Auth/Message.ML Wed Jun 24 11:24:52 1998 +0200
@@ -19,15 +19,15 @@
AddIffs msg.inject;
(*Equations hold because constructors are injective; cannot prove for all f*)
-goal thy "(Friend x : Friend``A) = (x:A)";
+Goal "(Friend x : Friend``A) = (x:A)";
by Auto_tac;
qed "Friend_image_eq";
-goal thy "(Key x : Key``A) = (x:A)";
+Goal "(Key x : Key``A) = (x:A)";
by Auto_tac;
qed "Key_image_eq";
-goal thy "(Nonce x ~: Key``A)";
+Goal "(Nonce x ~: Key``A)";
by Auto_tac;
qed "Nonce_Key_image_eq";
Addsimps [Friend_image_eq, Key_image_eq, Nonce_Key_image_eq];
@@ -35,7 +35,7 @@
(** Inverse of keys **)
-goal thy "!!K K'. (invKey K = invKey K') = (K=K')";
+Goal "!!K K'. (invKey K = invKey K') = (K=K')";
by Safe_tac;
by (rtac box_equals 1);
by (REPEAT (rtac invKey 2));
@@ -47,48 +47,48 @@
(**** keysFor operator ****)
-goalw thy [keysFor_def] "keysFor {} = {}";
+Goalw [keysFor_def] "keysFor {} = {}";
by (Blast_tac 1);
qed "keysFor_empty";
-goalw thy [keysFor_def] "keysFor (H Un H') = keysFor H Un keysFor H'";
+Goalw [keysFor_def] "keysFor (H Un H') = keysFor H Un keysFor H'";
by (Blast_tac 1);
qed "keysFor_Un";
-goalw thy [keysFor_def] "keysFor (UN i:A. H i) = (UN i:A. keysFor (H i))";
+Goalw [keysFor_def] "keysFor (UN i:A. H i) = (UN i:A. keysFor (H i))";
by (Blast_tac 1);
qed "keysFor_UN";
(*Monotonicity*)
-goalw thy [keysFor_def] "!!G H. G<=H ==> keysFor(G) <= keysFor(H)";
+Goalw [keysFor_def] "!!G H. G<=H ==> keysFor(G) <= keysFor(H)";
by (Blast_tac 1);
qed "keysFor_mono";
-goalw thy [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H";
+Goalw [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H";
by (Blast_tac 1);
qed "keysFor_insert_Agent";
-goalw thy [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H";
+Goalw [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H";
by (Blast_tac 1);
qed "keysFor_insert_Nonce";
-goalw thy [keysFor_def] "keysFor (insert (Number N) H) = keysFor H";
+Goalw [keysFor_def] "keysFor (insert (Number N) H) = keysFor H";
by (Blast_tac 1);
qed "keysFor_insert_Number";
-goalw thy [keysFor_def] "keysFor (insert (Key K) H) = keysFor H";
+Goalw [keysFor_def] "keysFor (insert (Key K) H) = keysFor H";
by (Blast_tac 1);
qed "keysFor_insert_Key";
-goalw thy [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H";
+Goalw [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H";
by (Blast_tac 1);
qed "keysFor_insert_Hash";
-goalw thy [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H";
+Goalw [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H";
by (Blast_tac 1);
qed "keysFor_insert_MPair";
-goalw thy [keysFor_def]
+Goalw [keysFor_def]
"keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)";
by Auto_tac;
qed "keysFor_insert_Crypt";
@@ -100,12 +100,12 @@
AddSEs [keysFor_Un RS equalityD1 RS subsetD RS UnE,
keysFor_UN RS equalityD1 RS subsetD RS UN_E];
-goalw thy [keysFor_def] "keysFor (Key``E) = {}";
+Goalw [keysFor_def] "keysFor (Key``E) = {}";
by Auto_tac;
qed "keysFor_image_Key";
Addsimps [keysFor_image_Key];
-goalw thy [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H";
+Goalw [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H";
by (Blast_tac 1);
qed "Crypt_imp_invKey_keysFor";
@@ -113,7 +113,7 @@
(**** Inductive relation "parts" ****)
val major::prems =
-goal thy "[| {|X,Y|} : parts H; \
+Goal "[| {|X,Y|} : parts H; \
\ [| X : parts H; Y : parts H |] ==> P \
\ |] ==> P";
by (cut_facts_tac [major] 1);
@@ -130,32 +130,32 @@
compound message. They work well on THIS FILE, perhaps because its
proofs concern only atomic messages.*)
-goal thy "H <= parts(H)";
+Goal "H <= parts(H)";
by (Blast_tac 1);
qed "parts_increasing";
(*Monotonicity*)
-goalw thy parts.defs "!!G H. G<=H ==> parts(G) <= parts(H)";
+Goalw parts.defs "!!G H. G<=H ==> parts(G) <= parts(H)";
by (rtac lfp_mono 1);
by (REPEAT (ares_tac basic_monos 1));
qed "parts_mono";
val parts_insertI = impOfSubs (subset_insertI RS parts_mono);
-goal thy "parts{} = {}";
+Goal "parts{} = {}";
by Safe_tac;
by (etac parts.induct 1);
by (ALLGOALS Blast_tac);
qed "parts_empty";
Addsimps [parts_empty];
-goal thy "!!X. X: parts{} ==> P";
+Goal "!!X. 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 thy "!!H. X: parts H ==> EX Y:H. X: parts {Y}";
+Goal "!!H. X: parts H ==> EX Y:H. X: parts {Y}";
by (etac parts.induct 1);
by (ALLGOALS Blast_tac);
qed "parts_singleton";
@@ -163,43 +163,43 @@
(** Unions **)
-goal thy "parts(G) Un parts(H) <= parts(G Un H)";
+Goal "parts(G) Un parts(H) <= parts(G Un H)";
by (REPEAT (ares_tac [Un_least, parts_mono, Un_upper1, Un_upper2] 1));
val parts_Un_subset1 = result();
-goal thy "parts(G Un H) <= parts(G) Un parts(H)";
+Goal "parts(G Un H) <= parts(G) Un parts(H)";
by (rtac subsetI 1);
by (etac parts.induct 1);
by (ALLGOALS Blast_tac);
val parts_Un_subset2 = result();
-goal thy "parts(G Un H) = parts(G) Un parts(H)";
+Goal "parts(G Un H) = parts(G) Un parts(H)";
by (REPEAT (ares_tac [equalityI, parts_Un_subset1, parts_Un_subset2] 1));
qed "parts_Un";
-goal thy "parts (insert X H) = parts {X} Un parts H";
+Goal "parts (insert X H) = parts {X} Un parts H";
by (stac (read_instantiate [("A","H")] insert_is_Un) 1);
by (simp_tac (HOL_ss addsimps [parts_Un]) 1);
qed "parts_insert";
(*TWO inserts to avoid looping. This rewrite is better than nothing.
Not suitable for Addsimps: its behaviour can be strange.*)
-goal thy "parts (insert X (insert Y H)) = parts {X} Un parts {Y} Un parts H";
+Goal "parts (insert X (insert Y H)) = parts {X} Un parts {Y} Un parts H";
by (simp_tac (simpset() addsimps [Un_assoc]) 1);
by (simp_tac (simpset() addsimps [parts_insert RS sym]) 1);
qed "parts_insert2";
-goal thy "(UN x:A. parts(H x)) <= parts(UN x:A. H x)";
+Goal "(UN x:A. parts(H x)) <= parts(UN x:A. H x)";
by (REPEAT (ares_tac [UN_least, parts_mono, UN_upper] 1));
val parts_UN_subset1 = result();
-goal thy "parts(UN x:A. H x) <= (UN x:A. parts(H x))";
+Goal "parts(UN x:A. H x) <= (UN x:A. parts(H x))";
by (rtac subsetI 1);
by (etac parts.induct 1);
by (ALLGOALS Blast_tac);
val parts_UN_subset2 = result();
-goal thy "parts(UN x:A. H x) = (UN x:A. parts(H x))";
+Goal "parts(UN x:A. H x) = (UN x:A. parts(H x))";
by (REPEAT (ares_tac [equalityI, parts_UN_subset1, parts_UN_subset2] 1));
qed "parts_UN";
@@ -209,36 +209,36 @@
AddSEs [parts_Un RS equalityD1 RS subsetD RS UnE,
parts_UN RS equalityD1 RS subsetD RS UN_E];
-goal thy "insert X (parts H) <= parts(insert X H)";
+Goal "insert X (parts H) <= parts(insert X H)";
by (blast_tac (claset() addIs [impOfSubs parts_mono]) 1);
qed "parts_insert_subset";
(** Idempotence and transitivity **)
-goal thy "!!H. X: parts (parts H) ==> X: parts H";
+Goal "!!H. X: parts (parts H) ==> X: parts H";
by (etac parts.induct 1);
by (ALLGOALS Blast_tac);
qed "parts_partsD";
AddSDs [parts_partsD];
-goal thy "parts (parts H) = parts H";
+Goal "parts (parts H) = parts H";
by (Blast_tac 1);
qed "parts_idem";
Addsimps [parts_idem];
-goal thy "!!H. [| X: parts G; G <= parts H |] ==> X: parts H";
+Goal "!!H. [| X: parts G; G <= parts H |] ==> X: parts H";
by (dtac parts_mono 1);
by (Blast_tac 1);
qed "parts_trans";
(*Cut*)
-goal thy "!!H. [| Y: parts (insert X G); X: parts H |] \
+Goal "!!H. [| 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 thy "!!H. X: parts H ==> parts (insert X H) = parts H";
+Goal "!!H. X: parts H ==> parts (insert X H) = parts H";
by (fast_tac (claset() addSDs [parts_cut]
addIs [parts_insertI]
addss (simpset())) 1);
@@ -254,27 +254,27 @@
etac parts.induct i,
REPEAT (Blast_tac i)];
-goal thy "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
+Goal "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
by (parts_tac 1);
qed "parts_insert_Agent";
-goal thy "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)";
+Goal "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)";
by (parts_tac 1);
qed "parts_insert_Nonce";
-goal thy "parts (insert (Number N) H) = insert (Number N) (parts H)";
+Goal "parts (insert (Number N) H) = insert (Number N) (parts H)";
by (parts_tac 1);
qed "parts_insert_Number";
-goal thy "parts (insert (Key K) H) = insert (Key K) (parts H)";
+Goal "parts (insert (Key K) H) = insert (Key K) (parts H)";
by (parts_tac 1);
qed "parts_insert_Key";
-goal thy "parts (insert (Hash X) H) = insert (Hash X) (parts H)";
+Goal "parts (insert (Hash X) H) = insert (Hash X) (parts H)";
by (parts_tac 1);
qed "parts_insert_Hash";
-goal thy "parts (insert (Crypt K X) H) = \
+Goal "parts (insert (Crypt K X) H) = \
\ insert (Crypt K X) (parts (insert X H))";
by (rtac equalityI 1);
by (rtac subsetI 1);
@@ -284,7 +284,7 @@
by (ALLGOALS (blast_tac (claset() addIs [parts.Body])));
qed "parts_insert_Crypt";
-goal thy "parts (insert {|X,Y|} H) = \
+Goal "parts (insert {|X,Y|} H) = \
\ insert {|X,Y|} (parts (insert X (insert Y H)))";
by (rtac equalityI 1);
by (rtac subsetI 1);
@@ -299,7 +299,7 @@
parts_insert_Hash, parts_insert_Crypt, parts_insert_MPair];
-goal thy "parts (Key``N) = Key``N";
+Goal "parts (Key``N) = Key``N";
by Auto_tac;
by (etac parts.induct 1);
by Auto_tac;
@@ -308,7 +308,7 @@
(*In any message, there is an upper bound N on its greatest nonce.*)
-goal thy "EX N. ALL n. N<=n --> Nonce n ~: parts {msg}";
+Goal "EX N. ALL n. N<=n --> Nonce n ~: parts {msg}";
by (induct_tac "msg" 1);
by (induct_tac "atomic" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [exI, parts_insert2])));
@@ -323,7 +323,7 @@
(**** Inductive relation "analz" ****)
val major::prems =
-goal thy "[| {|X,Y|} : analz H; \
+Goal "[| {|X,Y|} : analz H; \
\ [| X : analz H; Y : analz H |] ==> P \
\ |] ==> P";
by (cut_facts_tac [major] 1);
@@ -337,11 +337,11 @@
Addsimps [analz.Inj];
-goal thy "H <= analz(H)";
+Goal "H <= analz(H)";
by (Blast_tac 1);
qed "analz_increasing";
-goal thy "analz H <= parts H";
+Goal "analz H <= parts H";
by (rtac subsetI 1);
by (etac analz.induct 1);
by (ALLGOALS Blast_tac);
@@ -350,7 +350,7 @@
bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD);
-goal thy "parts (analz H) = parts H";
+Goal "parts (analz H) = parts H";
by (rtac equalityI 1);
by (rtac (analz_subset_parts RS parts_mono RS subset_trans) 1);
by (Simp_tac 1);
@@ -358,7 +358,7 @@
qed "parts_analz";
Addsimps [parts_analz];
-goal thy "analz (parts H) = parts H";
+Goal "analz (parts H) = parts H";
by Auto_tac;
by (etac analz.induct 1);
by Auto_tac;
@@ -366,7 +366,7 @@
Addsimps [analz_parts];
(*Monotonicity; Lemma 1 of Lowe*)
-goalw thy analz.defs "!!G H. G<=H ==> analz(G) <= analz(H)";
+Goalw analz.defs "!!G H. G<=H ==> analz(G) <= analz(H)";
by (rtac lfp_mono 1);
by (REPEAT (ares_tac basic_monos 1));
qed "analz_mono";
@@ -375,7 +375,7 @@
(** General equational properties **)
-goal thy "analz{} = {}";
+Goal "analz{} = {}";
by Safe_tac;
by (etac analz.induct 1);
by (ALLGOALS Blast_tac);
@@ -384,11 +384,11 @@
(*Converse fails: we can analz more from the union than from the
separate parts, as a key in one might decrypt a message in the other*)
-goal thy "analz(G) Un analz(H) <= analz(G Un H)";
+Goal "analz(G) Un analz(H) <= analz(G Un H)";
by (REPEAT (ares_tac [Un_least, analz_mono, Un_upper1, Un_upper2] 1));
qed "analz_Un";
-goal thy "insert X (analz H) <= analz(insert X H)";
+Goal "insert X (analz H) <= analz(insert X H)";
by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
qed "analz_insert";
@@ -399,30 +399,30 @@
etac analz.induct i,
REPEAT (Blast_tac i)];
-goal thy "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
+Goal "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
by (analz_tac 1);
qed "analz_insert_Agent";
-goal thy "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)";
+Goal "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)";
by (analz_tac 1);
qed "analz_insert_Nonce";
-goal thy "analz (insert (Number N) H) = insert (Number N) (analz H)";
+Goal "analz (insert (Number N) H) = insert (Number N) (analz H)";
by (analz_tac 1);
qed "analz_insert_Number";
-goal thy "analz (insert (Hash X) H) = insert (Hash X) (analz H)";
+Goal "analz (insert (Hash X) H) = insert (Hash X) (analz H)";
by (analz_tac 1);
qed "analz_insert_Hash";
(*Can only pull out Keys if they are not needed to decrypt the rest*)
-goalw thy [keysFor_def]
+Goalw [keysFor_def]
"!!K. K ~: keysFor (analz H) ==> \
\ analz (insert (Key K) H) = insert (Key K) (analz H)";
by (analz_tac 1);
qed "analz_insert_Key";
-goal thy "analz (insert {|X,Y|} H) = \
+Goal "analz (insert {|X,Y|} H) = \
\ insert {|X,Y|} (analz (insert X (insert Y H)))";
by (rtac equalityI 1);
by (rtac subsetI 1);
@@ -433,13 +433,13 @@
qed "analz_insert_MPair";
(*Can pull out enCrypted message if the Key is not known*)
-goal thy "!!H. Key (invKey K) ~: analz H ==> \
+Goal "!!H. 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 thy "!!H. Key (invKey K) : analz H ==> \
+Goal "!!H. 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 thy "!!H. Key (invKey K) : analz H ==> \
+Goal "!!H. 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 thy "!!H. Key (invKey K) : analz H ==> \
+Goal "!!H. 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));
@@ -466,7 +466,7 @@
Effective, but can cause subgoals to blow up!
Use with split_if; apparently split_tac does not cope with patterns
such as "analz (insert (Crypt K X) H)" *)
-goal thy "analz (insert (Crypt K X) H) = \
+Goal "analz (insert (Crypt K X) H) = \
\ (if (Key (invKey K) : analz H) \
\ then insert (Crypt K X) (analz (insert X H)) \
\ else insert (Crypt K X) (analz H))";
@@ -480,7 +480,7 @@
analz_insert_Hash, analz_insert_MPair, analz_Crypt_if];
(*This rule supposes "for the sake of argument" that we have the key.*)
-goal thy "analz (insert (Crypt K X) H) <= \
+Goal "analz (insert (Crypt K X) H) <= \
\ insert (Crypt K X) (analz (insert X H))";
by (rtac subsetI 1);
by (etac analz.induct 1);
@@ -488,7 +488,7 @@
qed "analz_insert_Crypt_subset";
-goal thy "analz (Key``N) = Key``N";
+Goal "analz (Key``N) = Key``N";
by Auto_tac;
by (etac analz.induct 1);
by Auto_tac;
@@ -499,24 +499,24 @@
(** Idempotence and transitivity **)
-goal thy "!!H. X: analz (analz H) ==> X: analz H";
+Goal "!!H. X: analz (analz H) ==> X: analz H";
by (etac analz.induct 1);
by (ALLGOALS Blast_tac);
qed "analz_analzD";
AddSDs [analz_analzD];
-goal thy "analz (analz H) = analz H";
+Goal "analz (analz H) = analz H";
by (Blast_tac 1);
qed "analz_idem";
Addsimps [analz_idem];
-goal thy "!!H. [| X: analz G; G <= analz H |] ==> X: analz H";
+Goal "!!H. [| 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 thy "!!H. [| Y: analz (insert X H); X: analz H |] ==> Y: analz H";
+Goal "!!H. [| Y: analz (insert X H); X: analz H |] ==> Y: analz H";
by (etac analz_trans 1);
by (Blast_tac 1);
qed "analz_cut";
@@ -528,34 +528,34 @@
(*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 thy "!!H. X: analz H ==> analz (insert X H) = analz H";
+Goal "!!H. 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 thy "!!H. [| analz G <= analz G'; analz H <= analz H' \
+Goal "!!H. [| 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 thy "!!H. [| analz G = analz G'; analz H = analz H' \
+Goal "!!H. [| 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 thy "!!H. analz H = analz H' ==> analz(insert X H) = analz(insert X H')";
+Goal "!!H. 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 thy "!!H. [| ALL X Y. {|X,Y|} ~: H; ALL X K. Crypt K X ~: H |] ==> \
+Goal "!!H. [| 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,12 +563,12 @@
qed "analz_trivial";
(*These two are obsolete (with a single Spy) but cost little to prove...*)
-goal thy "!!X. X: analz (UN i:A. analz (H i)) ==> X: analz (UN i:A. H i)";
+Goal "!!X. 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();
-goal thy "analz (UN i:A. analz (H i)) = analz (UN i:A. H i)";
+Goal "analz (UN i:A. analz (H i)) = analz (UN i:A. H i)";
by (blast_tac (claset() addIs [lemma, impOfSubs analz_mono]) 1);
qed "analz_UN_analz";
Addsimps [analz_UN_analz];
@@ -591,12 +591,12 @@
AddSEs [Nonce_synth, Key_synth, Hash_synth, MPair_synth, Crypt_synth];
-goal thy "H <= synth(H)";
+Goal "H <= synth(H)";
by (Blast_tac 1);
qed "synth_increasing";
(*Monotonicity*)
-goalw thy synth.defs "!!G H. G<=H ==> synth(G) <= synth(H)";
+Goalw synth.defs "!!G H. G<=H ==> synth(G) <= synth(H)";
by (rtac lfp_mono 1);
by (REPEAT (ares_tac basic_monos 1));
qed "synth_mono";
@@ -605,54 +605,54 @@
(*Converse fails: we can synth more from the union than from the
separate parts, building a compound message using elements of each.*)
-goal thy "synth(G) Un synth(H) <= synth(G Un H)";
+Goal "synth(G) Un synth(H) <= synth(G Un H)";
by (REPEAT (ares_tac [Un_least, synth_mono, Un_upper1, Un_upper2] 1));
qed "synth_Un";
-goal thy "insert X (synth H) <= synth(insert X H)";
+Goal "insert X (synth H) <= synth(insert X H)";
by (blast_tac (claset() addIs [impOfSubs synth_mono]) 1);
qed "synth_insert";
(** Idempotence and transitivity **)
-goal thy "!!H. X: synth (synth H) ==> X: synth H";
+Goal "!!H. X: synth (synth H) ==> X: synth H";
by (etac synth.induct 1);
by (ALLGOALS Blast_tac);
qed "synth_synthD";
AddSDs [synth_synthD];
-goal thy "synth (synth H) = synth H";
+Goal "synth (synth H) = synth H";
by (Blast_tac 1);
qed "synth_idem";
-goal thy "!!H. [| X: synth G; G <= synth H |] ==> X: synth H";
+Goal "!!H. [| 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 thy "!!H. [| Y: synth (insert X H); X: synth H |] ==> Y: synth H";
+Goal "!!H. [| Y: synth (insert X H); X: synth H |] ==> Y: synth H";
by (etac synth_trans 1);
by (Blast_tac 1);
qed "synth_cut";
-goal thy "Agent A : synth H";
+Goal "Agent A : synth H";
by (Blast_tac 1);
qed "Agent_synth";
-goal thy "Number n : synth H";
+Goal "Number n : synth H";
by (Blast_tac 1);
qed "Number_synth";
-goal thy "(Nonce N : synth H) = (Nonce N : H)";
+Goal "(Nonce N : synth H) = (Nonce N : H)";
by (Blast_tac 1);
qed "Nonce_synth_eq";
-goal thy "(Key K : synth H) = (Key K : H)";
+Goal "(Key K : synth H) = (Key K : H)";
by (Blast_tac 1);
qed "Key_synth_eq";
-goal thy "!!K. Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X : H)";
+Goal "!!K. Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X : H)";
by (Blast_tac 1);
qed "Crypt_synth_eq";
@@ -660,7 +660,7 @@
Nonce_synth_eq, Key_synth_eq, Crypt_synth_eq];
-goalw thy [keysFor_def]
+Goalw [keysFor_def]
"keysFor (synth H) = keysFor H Un invKey``{K. Key K : H}";
by (Blast_tac 1);
qed "keysFor_synth";
@@ -669,7 +669,7 @@
(*** Combinations of parts, analz and synth ***)
-goal thy "parts (synth H) = parts H Un synth H";
+Goal "parts (synth H) = parts H Un synth H";
by (rtac equalityI 1);
by (rtac subsetI 1);
by (etac parts.induct 1);
@@ -679,12 +679,12 @@
qed "parts_synth";
Addsimps [parts_synth];
-goal thy "analz (analz G Un H) = analz (G Un H)";
+Goal "analz (analz G Un H) = analz (G Un H)";
by (REPEAT_FIRST (resolve_tac [equalityI, analz_subset_cong]));
by (ALLGOALS Simp_tac);
qed "analz_analz_Un";
-goal thy "analz (synth G Un H) = analz (G Un H) Un synth G";
+Goal "analz (synth G Un H) = analz (G Un H) Un synth G";
by (rtac equalityI 1);
by (rtac subsetI 1);
by (etac analz.induct 1);
@@ -692,7 +692,7 @@
by (ALLGOALS (blast_tac (claset() addIs analz.intrs)));
qed "analz_synth_Un";
-goal thy "analz (synth H) = analz H Un synth H";
+Goal "analz (synth H) = analz H Un synth H";
by (cut_inst_tac [("H","{}")] analz_synth_Un 1);
by (Full_simp_tac 1);
qed "analz_synth";
@@ -701,14 +701,14 @@
(** For reasoning about the Fake rule in traces **)
-goal thy "!!Y. X: G ==> parts(insert X H) <= parts G Un parts H";
+Goal "!!Y. 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 thy "!!H. X: synth (analz H) ==> \
+Goal "!!H. 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);
@@ -716,7 +716,7 @@
qed "Fake_parts_insert";
(*H is sometimes (Key `` KK Un spies evs), so can't put G=H*)
-goal thy "!!H. X: synth (analz G) ==> \
+Goal "!!H. 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);
@@ -726,11 +726,11 @@
by (Blast_tac 1);
qed "Fake_analz_insert";
-goal thy "(X: analz H & X: parts H) = (X: analz H)";
+Goal "(X: analz H & X: parts H) = (X: analz H)";
by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1);
val analz_conj_parts = result();
-goal thy "(X: analz H | X: parts H) = (X: parts H)";
+Goal "(X: analz H | X: parts H) = (X: parts H)";
by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1);
val analz_disj_parts = result();
@@ -738,20 +738,20 @@
(*Without this equation, other rules for synth and analz would yield
redundant cases*)
-goal thy "({|X,Y|} : synth (analz H)) = \
+Goal "({|X,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 thy "!!K. [| Key K : analz H; Key (invKey K) : analz H |] \
+Goal "!!K. [| 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 thy "!!K. X ~: synth (analz H) \
+Goal "!!K. X ~: synth (analz H) \
\ ==> (Hash{|X,Y|} : synth (analz H)) = (Hash{|X,Y|} : analz H)";
by (Blast_tac 1);
qed "Hash_synth_analz";
@@ -762,27 +762,27 @@
(*** Freeness ***)
-goalw thy [HPair_def] "Agent A ~= Hash[X] Y";
+Goalw [HPair_def] "Agent A ~= Hash[X] Y";
by (Simp_tac 1);
qed "Agent_neq_HPair";
-goalw thy [HPair_def] "Nonce N ~= Hash[X] Y";
+Goalw [HPair_def] "Nonce N ~= Hash[X] Y";
by (Simp_tac 1);
qed "Nonce_neq_HPair";
-goalw thy [HPair_def] "Number N ~= Hash[X] Y";
+Goalw [HPair_def] "Number N ~= Hash[X] Y";
by (Simp_tac 1);
qed "Number_neq_HPair";
-goalw thy [HPair_def] "Key K ~= Hash[X] Y";
+Goalw [HPair_def] "Key K ~= Hash[X] Y";
by (Simp_tac 1);
qed "Key_neq_HPair";
-goalw thy [HPair_def] "Hash Z ~= Hash[X] Y";
+Goalw [HPair_def] "Hash Z ~= Hash[X] Y";
by (Simp_tac 1);
qed "Hash_neq_HPair";
-goalw thy [HPair_def] "Crypt K X' ~= Hash[X] Y";
+Goalw [HPair_def] "Crypt K X' ~= Hash[X] Y";
by (Simp_tac 1);
qed "Crypt_neq_HPair";
@@ -792,15 +792,15 @@
AddIffs HPair_neqs;
AddIffs (HPair_neqs RL [not_sym]);
-goalw thy [HPair_def] "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)";
+Goalw [HPair_def] "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)";
by (Simp_tac 1);
qed "HPair_eq";
-goalw thy [HPair_def] "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)";
+Goalw [HPair_def] "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)";
by (Simp_tac 1);
qed "MPair_eq_HPair";
-goalw thy [HPair_def] "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)";
+Goalw [HPair_def] "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)";
by Auto_tac;
qed "HPair_eq_MPair";
@@ -809,23 +809,23 @@
(*** Specialized laws, proved in terms of those for Hash and MPair ***)
-goalw thy [HPair_def] "keysFor (insert (Hash[X] Y) H) = keysFor H";
+Goalw [HPair_def] "keysFor (insert (Hash[X] Y) H) = keysFor H";
by (Simp_tac 1);
qed "keysFor_insert_HPair";
-goalw thy [HPair_def]
+Goalw [HPair_def]
"parts (insert (Hash[X] Y) H) = \
\ insert (Hash[X] Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))";
by (Simp_tac 1);
qed "parts_insert_HPair";
-goalw thy [HPair_def]
+Goalw [HPair_def]
"analz (insert (Hash[X] Y) H) = \
\ insert (Hash[X] Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))";
by (Simp_tac 1);
qed "analz_insert_HPair";
-goalw thy [HPair_def] "!!H. X ~: synth (analz H) \
+Goalw [HPair_def] "!!H. 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 Wed Jun 24 10:33:42 1998 +0200
+++ b/src/HOL/Auth/NS_Public.ML Wed Jun 24 11:24:52 1998 +0200
@@ -19,7 +19,7 @@
AddIffs [Spy_in_bad];
(*A "possibility property": there are traces that reach the end*)
-goal thy
+Goal
"!!A B. 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));
@@ -31,7 +31,7 @@
(**** Inductive proofs about ns_public ****)
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set evs";
+Goal "!!evs. 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,14 +54,14 @@
sends messages containing X! **)
(*Spy never sees another agent's private key! (unless it's bad at start)*)
-goal thy
+Goal
"!!A. 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 thy
+Goal
"!!A. evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
by Auto_tac;
qed "Spy_analz_priK";
@@ -75,7 +75,7 @@
(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
is secret. (Honest users generate fresh nonces.)*)
-goal thy
+Goal
"!!evs. [| 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)";
@@ -90,7 +90,7 @@
(*Unicity for NS1: nonce NA identifies agents A and B*)
-goal thy
+Goal
"!!evs. [| Nonce NA ~: analz (spies evs); evs : ns_public |] \
\ ==> EX A' B'. ALL A B. \
\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \
@@ -105,7 +105,7 @@
by (Blast_tac 1);
val lemma = result();
-goal thy
+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); \
@@ -122,7 +122,7 @@
(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
-goal thy
+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)";
@@ -141,7 +141,7 @@
(*Authentication for A: if she receives message 2 and has used NA
to start a run, then B has sent message 2.*)
-goal thy
+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; \
@@ -161,7 +161,7 @@
(*If the encrypted message appears then it originated with Alice in NS1*)
-goal thy
+Goal
"!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \
\ Nonce NA ~: analz (spies evs); \
\ evs : ns_public |] \
@@ -179,7 +179,7 @@
(*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 thy
+Goal
"!!evs. [| 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) \
@@ -194,7 +194,7 @@
by (Blast_tac 1);
val lemma = result();
-goal thy
+Goal
"!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|} \
\ : parts(spies evs); \
\ Crypt(pubK A') {|Nonce NA', Nonce NB, Agent B'|} \
@@ -209,7 +209,7 @@
(*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*)
-goal thy
+Goal
"!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
\ : set evs; \
\ A ~: bad; B ~: bad; evs : ns_public |] \
@@ -231,7 +231,7 @@
(*Authentication for B: if he receives message 3 and has used NB
in message 2, then A has sent message 3.*)
-goal thy
+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; \
@@ -255,7 +255,7 @@
(*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 thy
+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/src/HOL/Auth/NS_Public_Bad.ML Wed Jun 24 10:33:42 1998 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.ML Wed Jun 24 11:24:52 1998 +0200
@@ -23,7 +23,7 @@
AddIffs [Spy_in_bad];
(*A "possibility property": there are traces that reach the end*)
-goal thy
+Goal
"!!A B. 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));
@@ -35,7 +35,7 @@
(**** Inductive proofs about ns_public ****)
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set evs";
+Goal "!!evs. 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,14 +58,14 @@
sends messages containing X! **)
(*Spy never sees another agent's private key! (unless it's bad at start)*)
-goal thy
+Goal
"!!A. 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 thy
+Goal
"!!A. evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
by Auto_tac;
qed "Spy_analz_priK";
@@ -79,7 +79,7 @@
(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
is secret. (Honest users generate fresh nonces.)*)
-goal thy
+Goal
"!!evs. [| 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)";
@@ -94,7 +94,7 @@
(*Unicity for NS1: nonce NA identifies agents A and B*)
-goal thy
+Goal
"!!evs. [| Nonce NA ~: analz (spies evs); evs : ns_public |] \
\ ==> EX A' B'. ALL A B. \
\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \
@@ -109,7 +109,7 @@
by (Blast_tac 1);
val lemma = result();
-goal thy
+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); \
@@ -126,7 +126,7 @@
(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
-goal thy
+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)";
@@ -145,7 +145,7 @@
(*Authentication for A: if she receives message 2 and has used NA
to start a run, then B has sent message 2.*)
-goal thy
+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 |] \
@@ -166,7 +166,7 @@
(*If the encrypted message appears then it originated with Alice in NS1*)
-goal thy
+Goal
"!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \
\ Nonce NA ~: analz (spies evs); \
\ evs : ns_public |] \
@@ -183,7 +183,7 @@
(*Unicity for NS2: nonce NB identifies nonce NA and agent A
[proof closely follows that for unique_NA] *)
-goal thy
+Goal
"!!evs. [| Nonce NB ~: analz (spies evs); evs : ns_public |] \
\ ==> EX A' NA'. ALL A NA. \
\ Crypt (pubK A) {|Nonce NA, Nonce NB|} : parts (spies evs) \
@@ -197,7 +197,7 @@
by (Blast_tac 1);
val lemma = result();
-goal thy
+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); \
@@ -208,7 +208,7 @@
(*NB remains secret PROVIDED Alice never responds with round 3*)
-goal thy
+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 |] \
@@ -232,7 +232,7 @@
(*Authentication for B: if he receives message 3 and has used NB
in message 2, then A has sent message 3--to somebody....*)
-goal thy
+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 |] \
@@ -254,7 +254,7 @@
(*Can we strengthen the secrecy theorem? NO*)
-goal thy
+Goal
"!!evs. [| A ~: bad; B ~: bad; evs : ns_public |] \
\ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs \
\ --> Nonce NB ~: analz (spies evs)";
--- a/src/HOL/Auth/NS_Shared.ML Wed Jun 24 10:33:42 1998 +0200
+++ b/src/HOL/Auth/NS_Shared.ML Wed Jun 24 11:24:52 1998 +0200
@@ -21,7 +21,7 @@
(*A "possibility property": there are traces that reach the end*)
-goal thy
+Goal
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX N K. EX evs: ns_shared. \
\ Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs";
@@ -31,7 +31,7 @@
by possibility_tac;
result();
-goal thy
+Goal
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX evs: ns_shared. \
\ Says A B (Crypt ?K {|Nonce ?N, Nonce ?N|}) : set evs";
@@ -43,7 +43,7 @@
(**** Inductive proofs about ns_shared ****)
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : ns_shared ==> ALL A X. Says A A X ~: set evs";
+Goal "!!evs. 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,12 +51,12 @@
AddSEs [not_Says_to_self RSN (2, rev_notE)];
(*For reasoning about the encrypted portion of message NS3*)
-goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set evs \
+Goal "!!evs. 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 thy
+Goal
"!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set evs \
\ ==> K : parts (spies evs)";
by (Blast_tac 1);
@@ -75,14 +75,14 @@
sends messages containing X! **)
(*Spy never sees another agent's shared key! (unless it's bad at start)*)
-goal thy
+Goal
"!!evs. 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 thy
+Goal
"!!evs. evs : ns_shared ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
by Auto_tac;
qed "Spy_analz_shrK";
@@ -93,7 +93,7 @@
(*Nobody can have used non-existent keys!*)
-goal thy "!!evs. evs : ns_shared ==> \
+Goal "!!evs. evs : ns_shared ==> \
\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*Fake*)
@@ -112,7 +112,7 @@
(** Lemmas concerning the form of items passed in messages **)
(*Describes the form of K, X and K' when the Server sends this message.*)
-goal thy
+Goal
"!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) : set evs; \
\ evs : ns_shared |] \
\ ==> K ~: range shrK & \
@@ -125,7 +125,7 @@
(*If the encrypted message appears then it originated with the Server*)
-goal thy
+Goal
"!!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|}) \
@@ -136,7 +136,7 @@
qed "A_trusts_NS2";
-goal thy
+Goal
"!!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|})";
@@ -147,7 +147,7 @@
(*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 thy
+Goal
"!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) \
\ : set evs; \
\ evs : ns_shared |] \
@@ -180,7 +180,7 @@
(*NOT useful in this form, but it says that session keys are not used
to encrypt messages containing other keys, in the actual protocol.
We require that agents should behave like this subsequently also.*)
-goal thy
+Goal
"!!evs. [| evs : ns_shared; Kab ~: range shrK |] ==> \
\ (Crypt KAB X) : parts (spies evs) & \
\ Key K : parts {X} --> Key K : parts (spies evs)";
@@ -196,7 +196,7 @@
(** Session keys are not used to encrypt other session keys **)
(*The equality makes the induction hypothesis easier to apply*)
-goal thy
+Goal
"!!evs. evs : ns_shared ==> \
\ ALL K KK. KK <= Compl (range shrK) --> \
\ (Key K : analz (Key``KK Un (spies evs))) = \
@@ -212,7 +212,7 @@
qed_spec_mp "analz_image_freshK";
-goal thy
+Goal
"!!evs. [| evs : ns_shared; KAB ~: range shrK |] ==> \
\ Key K : analz (insert (Key KAB) (spies evs)) = \
\ (K = KAB | Key K : analz (spies evs))";
@@ -222,7 +222,7 @@
(** The session key K uniquely identifies the message **)
-goal thy
+Goal
"!!evs. 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 \
@@ -240,7 +240,7 @@
val lemma = result();
(*In messages of this form, the session key uniquely identifies the rest*)
-goal thy
+Goal
"!!evs. [| Says Server A \
\ (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs; \
\ Says Server A' \
@@ -252,7 +252,7 @@
(** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
-goal thy
+Goal
"!!evs. [| A ~: bad; B ~: bad; evs : ns_shared |] \
\ ==> Says Server A \
\ (Crypt (shrK A) {|NA, Agent B, Key K, \
@@ -285,7 +285,7 @@
(*Final version: Server's message in the most abstract form*)
-goal thy
+Goal
"!!evs. [| Says Server A \
\ (Crypt K' {|NA, Agent B, Key K, X|}) : set evs; \
\ ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \
@@ -302,7 +302,7 @@
(*If the encrypted message appears then it originated with the Server*)
-goal thy
+Goal
"!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs); \
\ B ~: bad; evs : ns_shared |] \
\ ==> EX NA. Says Server A \
@@ -315,7 +315,7 @@
qed "B_trusts_NS3";
-goal thy
+Goal
"!!evs. [| Crypt K (Nonce NB) : parts (spies evs); \
\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
\ : set evs; \
@@ -342,7 +342,7 @@
(*This version no longer assumes that K is secure*)
-goal thy
+Goal
"!!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; \
@@ -356,7 +356,7 @@
(*If the session key has been used in NS4 then somebody has forwarded
component X in some instance of NS4. Perhaps an interesting property,
but not needed (after all) for the proofs below.*)
-goal thy
+Goal
"!!evs. [| Crypt K (Nonce NB) : parts (spies evs); \
\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
\ : set evs; \
@@ -383,7 +383,7 @@
qed "NS4_implies_NS3";
-goal thy
+Goal
"!!evs. [| B ~: bad; evs : ns_shared |] \
\ ==> Key K ~: analz (spies evs) --> \
\ Says Server A \
@@ -411,7 +411,7 @@
(*Very strong Oops condition reveals protocol's weakness*)
-goal thy
+Goal
"!!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); \
--- a/src/HOL/Auth/OtwayRees.ML Wed Jun 24 10:33:42 1998 +0200
+++ b/src/HOL/Auth/OtwayRees.ML Wed Jun 24 11:24:52 1998 +0200
@@ -23,7 +23,7 @@
(*A "possibility property": there are traces that reach the end*)
-goal thy
+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|}|} \
@@ -37,7 +37,7 @@
(**** Inductive proofs about otway ****)
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs";
+Goal "!!evs. 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,19 +47,19 @@
(** For reasoning about the encrypted portion of messages **)
-goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \
+Goal "!!evs. 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 thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
+Goal "!!evs. 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 thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
+Goal "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
\ ==> K : parts (spies evs)";
by (Blast_tac 1);
qed "Oops_parts_spies";
@@ -82,14 +82,14 @@
sends messages containing X! **)
(*Spy never sees a good agent's shared key!*)
-goal thy
+Goal
"!!evs. 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 thy
+Goal
"!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
qed "Spy_analz_shrK";
@@ -100,7 +100,7 @@
(*Nobody can have used non-existent keys!*)
-goal thy "!!evs. evs : otway ==> \
+Goal "!!evs. evs : otway ==> \
\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*Fake*)
@@ -121,7 +121,7 @@
(*Describes the form of K and NA when the Server sends this message. Also
for Oops case.*)
-goal thy
+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)";
@@ -153,7 +153,7 @@
(** Session keys are not used to encrypt other session keys **)
(*The equality makes the induction hypothesis easier to apply*)
-goal thy
+Goal
"!!evs. evs : otway ==> \
\ ALL K KK. KK <= Compl (range shrK) --> \
\ (Key K : analz (Key``KK Un (spies evs))) = \
@@ -168,7 +168,7 @@
qed_spec_mp "analz_image_freshK";
-goal thy
+Goal
"!!evs. [| evs : otway; KAB ~: range shrK |] ==> \
\ Key K : analz (insert (Key KAB) (spies evs)) = \
\ (K = KAB | Key K : analz (spies evs))";
@@ -178,7 +178,7 @@
(*** The Key K uniquely identifies the Server's message. **)
-goal thy
+Goal
"!!evs. evs : otway ==> \
\ EX B' NA' NB' X'. ALL B NA NB X. \
\ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \
@@ -195,7 +195,7 @@
by (blast_tac (claset() addSEs spies_partsEs) 1);
val lemma = result();
-goal thy
+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'";
@@ -207,7 +207,7 @@
(**** Authenticity properties relating to NA ****)
(*Only OR1 can have caused such a part of a message to appear.*)
-goal thy
+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, \
@@ -220,7 +220,7 @@
(** The Nonce NA uniquely identifies A's message. **)
-goal thy
+Goal
"!!evs. [| evs : otway; A ~: bad |] \
\ ==> EX B'. ALL B. \
\ Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) \
@@ -233,7 +233,7 @@
by (Blast_tac 1);
val lemma = result();
-goal thy
+Goal
"!!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 |] \
@@ -245,7 +245,7 @@
(*It is impossible to re-use a nonce in both OR1 and OR2. This holds because
OR2 encrypts Nonce NB. It prevents the attack that can occur in the
over-simplified version of this protocol: see OtwayRees_Bad.*)
-goal thy
+Goal
"!!evs. [| A ~: bad; evs : otway |] \
\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
\ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \
@@ -258,7 +258,7 @@
(*Crucial property: If the encrypted message appears, and A has used NA
to start a run, then it originated with the Server!*)
-goal thy
+Goal
"!!evs. [| A ~: bad; evs : otway |] \
\ ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs) \
\ --> Says A B {|NA, Agent A, Agent B, \
@@ -290,7 +290,7 @@
then the key really did come from the Server! CANNOT prove this of the
bad form of this protocol, even though we can prove
Spy_not_see_encrypted_key*)
-goal thy
+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; \
@@ -308,7 +308,7 @@
Does not in itself guarantee security: an attack could violate
the premises, e.g. by having A=Spy **)
-goal thy
+Goal
"!!evs. [| A ~: bad; B ~: bad; evs : otway |] \
\ ==> Says Server B \
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
@@ -331,7 +331,7 @@
by (spy_analz_tac 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
-goal thy
+Goal
"!!evs. [| Says Server B \
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \
@@ -345,7 +345,7 @@
(*A's guarantee. The Oops premise quantifies over NB because A cannot know
what it is.*)
-goal thy
+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; \
@@ -360,7 +360,7 @@
(*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 thy
+Goal
"!!evs. [| B ~: bad; evs : otway |] \
\ ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \
\ : parts (spies evs) --> \
@@ -375,7 +375,7 @@
(** The Nonce NB uniquely identifies B's message. **)
-goal thy
+Goal
"!!evs. [| evs : otway; B ~: bad |] \
\ ==> EX NA' A'. ALL NA A. \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs) \
@@ -388,7 +388,7 @@
by (Blast_tac 1);
val lemma = result();
-goal thy
+Goal
"!!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 |] \
@@ -399,7 +399,7 @@
(*If the encrypted message appears, and B has used Nonce NB,
then it originated with the Server!*)
-goal thy
+Goal
"!!evs. [| B ~: bad; evs : otway |] \
\ ==> Crypt (shrK B) {|NB, Key K|} : parts (spies evs) \
\ --> (ALL X'. Says B Server \
@@ -430,7 +430,7 @@
(*Guarantee for B: if it gets a message with matching NB then the Server
has sent the correct message.*)
-goal thy
+Goal
"!!evs. [| Says B Server {|NA, Agent A, Agent B, X', \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
\ : set evs; \
@@ -446,7 +446,7 @@
(*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*)
-goal thy
+Goal
"!!evs. [| Says B Server {|NA, Agent A, Agent B, X', \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
\ : set evs; \
@@ -458,7 +458,7 @@
qed "B_gets_good_key";
-goal thy
+Goal
"!!evs. [| B ~: bad; evs : otway |] \
\ ==> Says Server B \
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
@@ -476,7 +476,7 @@
(*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 thy
+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/src/HOL/Auth/OtwayRees_AN.ML Wed Jun 24 10:33:42 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML Wed Jun 24 11:24:52 1998 +0200
@@ -23,7 +23,7 @@
(*A "possibility property": there are traces that reach the end*)
-goal thy
+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|}) \
@@ -37,7 +37,7 @@
(**** Inductive proofs about otway ****)
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs";
+Goal "!!evs. 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,13 +47,13 @@
(** For reasoning about the encrypted portion of messages **)
-goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \
+Goal "!!evs. 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 thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
+Goal "!!evs. 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,14 +73,14 @@
sends messages containing X! **)
(*Spy never sees a good agent's shared key!*)
-goal thy
+Goal
"!!evs. 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 thy
+Goal
"!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
qed "Spy_analz_shrK";
@@ -91,7 +91,7 @@
(*Nobody can have used non-existent keys!*)
-goal thy "!!evs. evs : otway ==> \
+Goal "!!evs. evs : otway ==> \
\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*Fake*)
@@ -111,7 +111,7 @@
(*** Proofs involving analz ***)
(*Describes the form of K and NA when the Server sends this message.*)
-goal thy
+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|}|} \
@@ -146,7 +146,7 @@
(** Session keys are not used to encrypt other session keys **)
(*The equality makes the induction hypothesis easier to apply*)
-goal thy
+Goal
"!!evs. evs : otway ==> \
\ ALL K KK. KK <= Compl (range shrK) --> \
\ (Key K : analz (Key``KK Un (spies evs))) = \
@@ -161,7 +161,7 @@
qed_spec_mp "analz_image_freshK";
-goal thy
+Goal
"!!evs. [| evs : otway; KAB ~: range shrK |] ==> \
\ Key K : analz (insert (Key KAB) (spies evs)) = \
\ (K = KAB | Key K : analz (spies evs))";
@@ -171,7 +171,7 @@
(*** The Key K uniquely identifies the Server's message. **)
-goal thy
+Goal
"!!evs. evs : otway ==> \
\ EX A' B' NA' NB'. ALL A B NA NB. \
\ Says Server B \
@@ -191,7 +191,7 @@
val lemma = result();
-goal thy
+Goal
"!!evs. [| Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} \
@@ -210,7 +210,7 @@
(**** Authenticity properties relating to NA ****)
(*If the encrypted message appears then it originated with the Server!*)
-goal thy
+Goal
"!!evs. [| A ~: bad; evs : otway |] \
\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} : parts (spies evs) \
\ --> (EX NB. Says Server B \
@@ -227,7 +227,7 @@
(*Corollary: if A receives B's OR4 message then it originated with the Server.
Freshness may be inferred from nonce NA.*)
-goal thy
+Goal
"!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \
\ : set evs; \
\ A ~: bad; evs : otway |] \
@@ -243,7 +243,7 @@
Does not in itself guarantee security: an attack could violate
the premises, e.g. by having A=Spy **)
-goal thy
+Goal
"!!evs. [| A ~: bad; B ~: bad; evs : otway |] \
\ ==> Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
@@ -267,7 +267,7 @@
by (spy_analz_tac 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
-goal thy
+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|}|} \
@@ -282,7 +282,7 @@
(*A's guarantee. The Oops premise quantifies over NB because A cannot know
what it is.*)
-goal thy
+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; \
@@ -295,7 +295,7 @@
(**** Authenticity properties relating to NB ****)
(*If the encrypted message appears then it originated with the Server!*)
-goal thy
+Goal
"!!evs. [| B ~: bad; evs : otway |] \
\ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} : parts (spies evs) \
\ --> (EX NA. Says Server B \
@@ -312,7 +312,7 @@
(*Guarantee for B: if it gets a well-formed certificate then the Server
has sent the correct message in round 3.*)
-goal thy
+Goal
"!!evs. [| Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set evs; \
\ B ~: bad; evs : otway |] \
@@ -325,7 +325,7 @@
(*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*)
-goal thy
+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/src/HOL/Auth/OtwayRees_Bad.ML Wed Jun 24 10:33:42 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Wed Jun 24 11:24:52 1998 +0200
@@ -26,7 +26,7 @@
(*A "possibility property": there are traces that reach the end*)
-goal thy
+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|}|} \
@@ -40,7 +40,7 @@
(**** Inductive proofs about otway ****)
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs";
+Goal "!!evs. 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,19 +50,19 @@
(** For reasoning about the encrypted portion of messages **)
-goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \
+Goal "!!evs. 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 thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
+Goal "!!evs. 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 thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
+Goal "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
\ ==> K : parts (spies evs)";
by (Blast_tac 1);
qed "Oops_parts_spies";
@@ -85,14 +85,14 @@
sends messages containing X! **)
(*Spy never sees a good agent's shared key!*)
-goal thy
+Goal
"!!evs. 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 thy
+Goal
"!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
qed "Spy_analz_shrK";
@@ -103,7 +103,7 @@
(*Nobody can have used non-existent keys!*)
-goal thy "!!evs. evs : otway ==> \
+Goal "!!evs. evs : otway ==> \
\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*Fake*)
@@ -124,7 +124,7 @@
(*Describes the form of K and NA when the Server sends this message. Also
for Oops case.*)
-goal thy
+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)";
@@ -156,7 +156,7 @@
(** Session keys are not used to encrypt other session keys **)
(*The equality makes the induction hypothesis easier to apply*)
-goal thy
+Goal
"!!evs. evs : otway ==> \
\ ALL K KK. KK <= Compl (range shrK) --> \
\ (Key K : analz (Key``KK Un (spies evs))) = \
@@ -171,7 +171,7 @@
qed_spec_mp "analz_image_freshK";
-goal thy
+Goal
"!!evs. [| evs : otway; KAB ~: range shrK |] ==> \
\ Key K : analz (insert (Key KAB) (spies evs)) = \
\ (K = KAB | Key K : analz (spies evs))";
@@ -181,7 +181,7 @@
(*** The Key K uniquely identifies the Server's message. **)
-goal thy
+Goal
"!!evs. evs : otway ==> \
\ EX B' NA' NB' X'. ALL B NA NB X. \
\ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \
@@ -198,7 +198,7 @@
by (blast_tac (claset() addSEs spies_partsEs) 1);
val lemma = result();
-goal thy
+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'";
@@ -210,7 +210,7 @@
Does not in itself guarantee security: an attack could violate
the premises, e.g. by having A=Spy **)
-goal thy
+Goal
"!!evs. [| A ~: bad; B ~: bad; evs : otway |] \
\ ==> Says Server B \
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
@@ -233,7 +233,7 @@
by (spy_analz_tac 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
-goal thy
+Goal
"!!evs. [| Says Server B \
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \
@@ -251,7 +251,7 @@
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 thy
+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, \
@@ -265,7 +265,7 @@
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 thy
+Goal
"!!evs. [| A ~: bad; evs : otway |] \
\ ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs) --> \
\ Says A B {|NA, Agent A, Agent B, \
--- a/src/HOL/Auth/Public.ML Wed Jun 24 10:33:42 1998 +0200
+++ b/src/HOL/Auth/Public.ML Wed Jun 24 11:24:52 1998 +0200
@@ -15,7 +15,7 @@
AddIffs [inj_pubK RS inj_eq];
-goal thy "!!A B. (priK A = priK B) = (A=B)";
+Goal "!!A B. (priK A = priK B) = (A=B)";
by Safe_tac;
by (dres_inst_tac [("f","invKey")] arg_cong 1);
by (Full_simp_tac 1);
@@ -24,11 +24,11 @@
AddIffs [priK_inj_eq];
AddIffs [priK_neq_pubK, priK_neq_pubK RS not_sym];
-goalw thy [isSymKey_def] "~ isSymKey (pubK A)";
+Goalw [isSymKey_def] "~ isSymKey (pubK A)";
by (Simp_tac 1);
qed "not_isSymKey_pubK";
-goalw thy [isSymKey_def] "~ isSymKey (priK A)";
+Goalw [isSymKey_def] "~ isSymKey (priK A)";
by (Simp_tac 1);
qed "not_isSymKey_priK";
@@ -37,16 +37,16 @@
(** "Image" equations that hold for injective functions **)
-goal thy "(invKey x : invKey``A) = (x:A)";
+Goal "(invKey x : invKey``A) = (x:A)";
by Auto_tac;
qed "invKey_image_eq";
(*holds because invKey is injective*)
-goal thy "(pubK x : pubK``A) = (x:A)";
+Goal "(pubK x : pubK``A) = (x:A)";
by Auto_tac;
qed "pubK_image_eq";
-goal thy "(priK x ~: pubK``A)";
+Goal "(priK x ~: pubK``A)";
by Auto_tac;
qed "priK_pubK_image_eq";
Addsimps [invKey_image_eq, pubK_image_eq, priK_pubK_image_eq];
@@ -55,7 +55,7 @@
(** Rewrites should not refer to initState(Friend i)
-- not in normal form! **)
-goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
+Goalw [keysFor_def] "keysFor (parts (initState C)) = {}";
by (induct_tac "C" 1);
by (auto_tac (claset() addIs [range_eqI], simpset()));
qed "keysFor_parts_initState";
@@ -65,14 +65,14 @@
(*** Function "spies" ***)
(*Agents see their own private keys!*)
-goal thy "Key (priK A) : initState A";
+Goal "Key (priK A) : initState A";
by (induct_tac "A" 1);
by Auto_tac;
qed "priK_in_initState";
AddIffs [priK_in_initState];
(*All public keys are visible*)
-goal thy "Key (pubK A) : spies evs";
+Goal "Key (pubK A) : spies evs";
by (induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac
(simpset() addsimps [imageI, spies_Cons]
@@ -80,7 +80,7 @@
qed_spec_mp "spies_pubK";
(*Spy sees private keys of bad agents!*)
-goal thy "!!A. A: bad ==> Key (priK A) : spies evs";
+Goal "!!A. A: bad ==> Key (priK A) : spies evs";
by (induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac
(simpset() addsimps [imageI, spies_Cons]
@@ -92,7 +92,7 @@
(*For not_bad_tac*)
-goal thy "!!A. [| Crypt (pubK A) X : analz (spies evs); A: bad |] \
+Goal "!!A. [| 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";
@@ -112,13 +112,13 @@
(*** Fresh nonces ***)
-goal thy "Nonce N ~: parts (initState B)";
+Goal "Nonce N ~: parts (initState B)";
by (induct_tac "B" 1);
by Auto_tac;
qed "Nonce_notin_initState";
AddIffs [Nonce_notin_initState];
-goal thy "Nonce N ~: used []";
+Goal "Nonce N ~: used []";
by (simp_tac (simpset() addsimps [used_Nil]) 1);
qed "Nonce_notin_used_empty";
Addsimps [Nonce_notin_used_empty];
@@ -127,7 +127,7 @@
(*** Supply fresh nonces for possibility theorems. ***)
(*In any trace, there is an upper bound N on the greatest nonce in use.*)
-goal thy "EX N. ALL n. N<=n --> Nonce n ~: used evs";
+Goal "EX N. ALL n. N<=n --> Nonce n ~: used evs";
by (induct_tac "evs" 1);
by (res_inst_tac [("x","0")] exI 1);
by (ALLGOALS (asm_simp_tac
@@ -138,12 +138,12 @@
by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
val lemma = result();
-goal thy "EX N. Nonce N ~: used evs";
+Goal "EX N. Nonce N ~: used evs";
by (rtac (lemma RS exE) 1);
by (Blast_tac 1);
qed "Nonce_supply1";
-goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
+Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
by (rtac (lemma RS exE) 1);
by (rtac selectI 1);
by (Fast_tac 1);
@@ -160,11 +160,11 @@
(*** Specialized rewriting for the analz_image_... theorems ***)
-goal thy "insert (Key K) H = Key `` {K} Un H";
+Goal "insert (Key K) H = Key `` {K} Un H";
by (Blast_tac 1);
qed "insert_Key_singleton";
-goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
+Goal "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
by (Blast_tac 1);
qed "insert_Key_image";
--- a/src/HOL/Auth/Recur.ML Wed Jun 24 10:33:42 1998 +0200
+++ b/src/HOL/Auth/Recur.ML Wed Jun 24 11:24:52 1998 +0200
@@ -20,7 +20,7 @@
(*Simplest case: Alice goes directly to the server*)
-goal thy
+Goal
"!!A. A ~= Server \
\ ==> EX K NA. EX evs: recur. \
\ Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
@@ -33,7 +33,7 @@
(*Case two: Alice, Bob and the server*)
-goal thy
+Goal
"!!A B. [| 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|}, \
@@ -52,7 +52,7 @@
(*Case three: Alice, Bob, Charlie and the server
TOO SLOW to run every time!
-goal thy
+Goal
"!!A B. [| 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|}, \
@@ -75,7 +75,7 @@
(**** Inductive proofs about recur ****)
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : recur ==> ALL A X. Says A A X ~: set evs";
+Goal "!!evs. 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,17 +84,17 @@
-goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB : parts{RB}";
+Goal "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB : parts{RB}";
by (etac respond.induct 1);
by (ALLGOALS Simp_tac);
qed "respond_Key_in_parts";
-goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB ~: used evs";
+Goal "!!evs. (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 thy
+Goal
"!!evs. [| Key K : parts {RB}; (PB,RB,K') : respond evs |] \
\ ==> Key K ~: used evs";
by (etac rev_mp 1);
@@ -104,7 +104,7 @@
qed_spec_mp "Key_in_parts_respond";
(*Simple inductive reasoning about responses*)
-goal thy "!!evs. (PA,RB,KAB) : respond evs ==> RB : responses evs";
+Goal "!!evs. (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,7 +114,7 @@
val RA2_analz_spies = Says_imp_spies RS analz.Inj |> standard;
-goal thy "!!evs. Says C' B {|Crypt K X, X', RA|} : set evs \
+Goal "!!evs. 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,7 +144,7 @@
(** Spy never sees another agent's shared key! (unless it's bad at start) **)
-goal thy
+Goal
"!!evs. evs : recur ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
@@ -155,7 +155,7 @@
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
-goal thy
+Goal
"!!evs. evs : recur ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
qed "Spy_analz_shrK";
@@ -168,7 +168,7 @@
(** Nobody can have used non-existent keys! **)
(*The special case of H={} has the same proof*)
-goal thy
+Goal
"!!evs. [| K : keysFor (parts (insert RB H)); (PB,RB,K') : respond evs |] \
\ ==> K : range shrK | K : keysFor (parts H)";
by (etac rev_mp 1);
@@ -177,7 +177,7 @@
qed_spec_mp "Key_in_keysFor_parts";
-goal thy "!!evs. evs : recur ==> \
+Goal "!!evs. evs : recur ==> \
\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*RA3*)
@@ -209,7 +209,7 @@
(*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 thy
+Goal
"!!evs. [| RB : responses evs; \
\ ALL K KK. KK <= Compl (range shrK) --> \
\ (Key K : analz (Key``KK Un H)) = \
@@ -222,7 +222,7 @@
qed "resp_analz_image_freshK_lemma";
(*Version for the protocol. Proof is almost trivial, thanks to the lemma.*)
-goal thy
+Goal
"!!evs. evs : recur ==> \
\ ALL K KK. KK <= Compl (range shrK) --> \
\ (Key K : analz (Key``KK Un (spies evs))) = \
@@ -250,7 +250,7 @@
raw_analz_image_freshK RSN
(2, resp_analz_image_freshK_lemma) RS spec RS spec RS mp);
-goal thy
+Goal
"!!evs. [| evs : recur; KAB ~: range shrK |] ==> \
\ Key K : analz (insert (Key KAB) (spies evs)) = \
\ (K = KAB | Key K : analz (spies evs))";
@@ -259,7 +259,7 @@
(*Everything that's hashed is already in past traffic. *)
-goal thy "!!evs. [| Hash {|Key(shrK A), X|} : parts (spies evs); \
+Goal "!!evs. [| Hash {|Key(shrK A), X|} : parts (spies evs); \
\ evs : recur; A ~: bad |] \
\ ==> X : parts (spies evs)";
by (etac rev_mp 1);
@@ -278,7 +278,7 @@
Unicity is not used in other proofs but is desirable in its own right.
**)
-goal thy
+Goal
"!!evs. [| evs : recur; A ~: bad |] \
\ ==> EX B' P'. ALL B P. \
\ Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (spies evs) \
@@ -295,7 +295,7 @@
addSEs spies_partsEs) 1));
val lemma = result();
-goalw thy [HPair_def]
+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 |] \
@@ -309,7 +309,7 @@
(relations "respond" and "responses")
***)
-goal thy
+Goal
"!!evs. [| RB : responses evs; evs : recur |] \
\ ==> (Key (shrK B) : analz (insert RB (spies evs))) = (B:bad)";
by (etac responses.induct 1);
@@ -321,7 +321,7 @@
Addsimps [shrK_in_analz_respond];
-goal thy
+Goal
"!!evs. [| RB : responses evs; \
\ ALL K KK. KK <= Compl (range shrK) --> \
\ (Key K : analz (Key``KK Un H)) = \
@@ -344,7 +344,7 @@
(*The Server does not send such messages. This theorem lets us avoid
assuming B~=Server in RA4.*)
-goal thy
+Goal
"!!evs. evs : recur \
\ ==> ALL C X Y. Says Server C {|X, Agent Server, Y|} ~: set evs";
by (etac recur.induct 1);
@@ -355,7 +355,7 @@
(*The last key returned by respond indeed appears in a certificate*)
-goal thy
+Goal
"!!K. (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);
@@ -363,7 +363,7 @@
qed "respond_certificate";
-goal thy
+Goal
"!!K'. (PB,RB,KXY) : respond evs \
\ ==> EX A' B'. ALL A B N. \
\ Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB} \
@@ -385,7 +385,7 @@
by (Fast_tac 1);
val lemma = result();
-goal thy
+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 |] \
@@ -398,7 +398,7 @@
Does not in itself guarantee security: an attack could violate
the premises, e.g. by having A=Spy **)
-goal thy
+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} --> \
@@ -429,7 +429,7 @@
qed_spec_mp "respond_Spy_not_see_session_key";
-goal thy
+Goal
"!!evs. [| Crypt (shrK A) {|Key K, Agent A', N|} : parts (spies evs); \
\ A ~: bad; A' ~: bad; evs : recur |] \
\ ==> Key K ~: analz (spies evs)";
@@ -463,7 +463,7 @@
(**** Authenticity properties for Agents ****)
(*The response never contains Hashes*)
-goal thy
+Goal
"!!evs. [| Hash {|Key (shrK B), M|} : parts (insert RB H); \
\ (PB,RB,K) : respond evs |] \
\ ==> Hash {|Key (shrK B), M|} : parts H";
@@ -476,7 +476,7 @@
This result is of no use to B, who cannot verify the Hash. Moreover,
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 thy [HPair_def]
+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";
@@ -493,7 +493,7 @@
(*Certificates can only originate with the Server.*)
-goal thy
+Goal
"!!evs. [| Crypt (shrK A) Y : parts (spies evs); \
\ A ~: bad; evs : recur |] \
\ ==> EX C RC. Says Server C RC : set evs & \
--- a/src/HOL/Auth/Shared.ML Wed Jun 24 10:33:42 1998 +0200
+++ b/src/HOL/Auth/Shared.ML Wed Jun 24 11:24:52 1998 +0200
@@ -22,14 +22,14 @@
(** Rewrites should not refer to initState(Friend i)
-- not in normal form! **)
-goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
+Goalw [keysFor_def] "keysFor (parts (initState C)) = {}";
by (induct_tac "C" 1);
by Auto_tac;
qed "keysFor_parts_initState";
Addsimps [keysFor_parts_initState];
(*Specialized to shared-key model: no need for addss in protocol proofs*)
-goal thy "!!X. [| K: keysFor (parts (insert X H)); X : synth (analz H) |] \
+Goal "!!X. [| 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 thy "!!H. Crypt K X : H ==> K : keysFor H";
+Goal "!!H. 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 thy "!!A. A: bad ==> Key (shrK A) : spies evs";
+Goal "!!A. 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 thy "!!A. [| Crypt (shrK A) X : analz (spies evs); A: bad |] \
+Goal "!!A. [| 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";
@@ -78,13 +78,13 @@
(** Fresh keys never clash with long-term shared keys **)
(*Agents see their own shared keys!*)
-goal thy "Key (shrK A) : initState A";
+Goal "Key (shrK A) : initState A";
by (induct_tac "A" 1);
by Auto_tac;
qed "shrK_in_initState";
AddIffs [shrK_in_initState];
-goal thy "Key (shrK A) : used evs";
+Goal "Key (shrK A) : used evs";
by (rtac initState_into_used 1);
by (Blast_tac 1);
qed "shrK_in_used";
@@ -92,11 +92,11 @@
(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
from long-term shared keys*)
-goal thy "!!K. Key K ~: used evs ==> K ~: range shrK";
+Goal "!!K. Key K ~: used evs ==> K ~: range shrK";
by (Blast_tac 1);
qed "Key_not_used";
-goal thy "!!K. Key K ~: used evs ==> shrK B ~= K";
+Goal "!!K. Key K ~: used evs ==> shrK B ~= K";
by (Blast_tac 1);
qed "shrK_neq";
@@ -105,13 +105,13 @@
(*** Fresh nonces ***)
-goal thy "Nonce N ~: parts (initState B)";
+Goal "Nonce N ~: parts (initState B)";
by (induct_tac "B" 1);
by Auto_tac;
qed "Nonce_notin_initState";
AddIffs [Nonce_notin_initState];
-goal thy "Nonce N ~: used []";
+Goal "Nonce N ~: used []";
by (simp_tac (simpset() addsimps [used_Nil]) 1);
qed "Nonce_notin_used_empty";
Addsimps [Nonce_notin_used_empty];
@@ -120,7 +120,7 @@
(*** Supply fresh nonces for possibility theorems. ***)
(*In any trace, there is an upper bound N on the greatest nonce in use.*)
-goal thy "EX N. ALL n. N<=n --> Nonce n ~: used evs";
+Goal "EX N. ALL n. N<=n --> Nonce n ~: used evs";
by (induct_tac "evs" 1);
by (res_inst_tac [("x","0")] exI 1);
by (ALLGOALS (asm_simp_tac
@@ -131,12 +131,12 @@
by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
val lemma = result();
-goal thy "EX N. Nonce N ~: used evs";
+Goal "EX N. Nonce N ~: used evs";
by (rtac (lemma RS exE) 1);
by (Blast_tac 1);
qed "Nonce_supply1";
-goal thy "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'";
+Goal "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'";
by (cut_inst_tac [("evs","evs")] lemma 1);
by (cut_inst_tac [("evs","evs'")] lemma 1);
by (Clarify_tac 1);
@@ -147,7 +147,7 @@
le_eq_less_Suc RS sym]) 1);
qed "Nonce_supply2";
-goal thy "EX N N' N''. Nonce N ~: used evs & Nonce N' ~: used evs' & \
+Goal "EX N N' N''. Nonce N ~: used evs & Nonce N' ~: used evs' & \
\ Nonce N'' ~: used evs'' & N ~= N' & N' ~= N'' & N ~= N''";
by (cut_inst_tac [("evs","evs")] lemma 1);
by (cut_inst_tac [("evs","evs'")] lemma 1);
@@ -161,7 +161,7 @@
le_eq_less_Suc RS sym]) 1);
qed "Nonce_supply3";
-goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
+Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
by (rtac (lemma RS exE) 1);
by (rtac selectI 1);
by (Blast_tac 1);
@@ -169,12 +169,12 @@
(*** Supply fresh keys for possibility theorems. ***)
-goal thy "EX K. Key K ~: used evs";
+Goal "EX K. Key K ~: used evs";
by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
by (Blast_tac 1);
qed "Key_supply1";
-goal thy "EX K K'. Key K ~: used evs & Key K' ~: used evs' & K ~= K'";
+Goal "EX K K'. Key K ~: used evs & Key K' ~: used evs' & K ~= K'";
by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
by (etac exE 1);
by (cut_inst_tac [("evs","evs'")]
@@ -182,7 +182,7 @@
by (Asm_full_simp_tac 1 THEN depth_tac (claset()) 2 1); (* replaces Auto_tac *)
qed "Key_supply2";
-goal thy "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \
+Goal "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \
\ Key K'' ~: used evs'' & K ~= K' & K' ~= K'' & K ~= K''";
by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
by (etac exE 1);
@@ -195,7 +195,7 @@
by (Blast_tac 1);
qed "Key_supply3";
-goal thy "Key (@ K. Key K ~: used evs) ~: used evs";
+Goal "Key (@ K. Key K ~: used evs) ~: used evs";
by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
by (rtac selectI 1);
by (Blast_tac 1);
@@ -223,15 +223,15 @@
(*** Specialized rewriting for analz_insert_freshK ***)
-goal thy "!!A. A <= Compl (range shrK) ==> shrK x ~: A";
+Goal "!!A. A <= Compl (range shrK) ==> shrK x ~: A";
by (Blast_tac 1);
qed "subset_Compl_range";
-goal thy "insert (Key K) H = Key `` {K} Un H";
+Goal "insert (Key K) H = Key `` {K} Un H";
by (Blast_tac 1);
qed "insert_Key_singleton";
-goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
+Goal "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
by (Blast_tac 1);
qed "insert_Key_image";
@@ -249,7 +249,7 @@
@disj_comms);
(*Lemma for the trivial direction of the if-and-only-if*)
-goal thy
+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)";
by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
--- a/src/HOL/Auth/TLS.ML Wed Jun 24 10:33:42 1998 +0200
+++ b/src/HOL/Auth/TLS.ML Wed Jun 24 11:24:52 1998 +0200
@@ -34,13 +34,13 @@
(*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
-goal thy "pubK A ~= sessionK arg";
+Goal "pubK A ~= sessionK arg";
by (rtac notI 1);
by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
by (Full_simp_tac 1);
qed "pubK_neq_sessionK";
-goal thy "priK A ~= sessionK arg";
+Goal "priK A ~= sessionK arg";
by (rtac notI 1);
by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
by (Full_simp_tac 1);
@@ -64,7 +64,7 @@
(*Possibility property ending with ClientAccepts.*)
-goal thy
+Goal
"!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \
\ A ~= B |] \
\ ==> EX SID M. EX evs: tls. \
@@ -78,7 +78,7 @@
result();
(*And one for ServerAccepts. Either FINISHED message may come first.*)
-goal thy
+Goal
"!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \
\ A ~= B |] \
\ ==> EX SID NA PA NB PB M. EX evs: tls. \
@@ -92,7 +92,7 @@
result();
(*Another one, for CertVerify (which is optional)*)
-goal thy
+Goal
"!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \
\ A ~= B |] \
\ ==> EX NB PMS. EX evs: tls. \
@@ -105,7 +105,7 @@
result();
(*Another one, for session resumption (both ServerResume and ClientResume) *)
-goal thy
+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; \
@@ -128,7 +128,7 @@
(**** Inductive proofs about tls ****)
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : tls ==> ALL A X. Says A A X ~: set evs";
+Goal "!!evs. 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,14 +152,14 @@
sends messages containing X! **)
(*Spy never sees another agent's private key! (unless it's bad at start)*)
-goal thy
+Goal
"!!evs. 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 thy
+Goal
"!!evs. evs : tls ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
qed "Spy_analz_priK";
@@ -173,7 +173,7 @@
model to include bogus certificates for the agents, but there seems
little point in doing so: the loss of their private keys is a worse
breach of security.*)
-goalw thy [certificate_def]
+Goalw [certificate_def]
"!!evs. [| certificate B KB : parts (spies evs); evs : tls |] \
\ ==> pubK B = KB";
by (etac rev_mp 1);
@@ -203,7 +203,7 @@
(*** Properties of items found in Notes ***)
-goal thy "!!evs. [| Notes A {|Agent B, X|} : set evs; evs : tls |] \
+Goal "!!evs. [| 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);
@@ -211,7 +211,7 @@
qed "Notes_Crypt_parts_spies";
(*C may be either A or B*)
-goal thy
+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)";
@@ -226,7 +226,7 @@
qed "Notes_master_imp_Crypt_PMS";
(*Compared with the theorem above, both premise and conclusion are stronger*)
-goal thy
+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";
@@ -240,7 +240,7 @@
(*** Protocol goal: if B receives CertVerify, then A sent it ***)
(*B can check A's signature if he has received A's certificate.*)
-goal thy
+Goal
"!!evs. [| X : parts (spies evs); \
\ X = Crypt (priK A) (Hash{|nb, Agent B, pms|}); \
\ evs : tls; A ~: bad |] \
@@ -252,7 +252,7 @@
val lemma = result();
(*Final version: B checks X using the distributed KA instead of priK A*)
-goal thy
+Goal
"!!evs. [| X : parts (spies evs); \
\ X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|}); \
\ certificate A KA : parts (spies evs); \
@@ -263,7 +263,7 @@
(*If CertVerify is present then A has chosen PMS.*)
-goal thy
+Goal
"!!evs. [| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|}) \
\ : parts (spies evs); \
\ evs : tls; A ~: bad |] \
@@ -274,7 +274,7 @@
val lemma = result();
(*Final version using the distributed KA instead of priK A*)
-goal thy
+Goal
"!!evs. [| Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}) \
\ : parts (spies evs); \
\ certificate A KA : parts (spies evs); \
@@ -284,7 +284,7 @@
qed "UseCertVerify";
-goal thy "!!evs. evs : tls ==> Notes A {|Agent B, Nonce (PRF x)|} ~: set evs";
+Goal "!!evs. 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,7 +292,7 @@
Addsimps [no_Notes_A_PRF];
-goal thy "!!evs. [| Nonce (PRF (PMS,NA,NB)) : parts (spies evs); \
+Goal "!!evs. [| Nonce (PRF (PMS,NA,NB)) : parts (spies evs); \
\ evs : tls |] \
\ ==> Nonce PMS : parts (spies evs)";
by (etac rev_mp 1);
@@ -309,7 +309,7 @@
(*** Unicity results for PMS, the pre-master-secret ***)
(*PMS determines B. Proof borrowed from NS_Public/unique_NA and from Yahalom*)
-goal thy
+Goal
"!!evs. [| Nonce PMS ~: analz (spies evs); evs : tls |] \
\ ==> EX B'. ALL B. \
\ Crypt (pubK B) (Nonce PMS) : parts (spies evs) --> B=B'";
@@ -323,7 +323,7 @@
blast_tac (claset() addSEs partsEs) 1);
val lemma = result();
-goal thy
+Goal
"!!evs. [| Crypt(pubK B) (Nonce PMS) : parts (spies evs); \
\ Crypt(pubK B') (Nonce PMS) : parts (spies evs); \
\ Nonce PMS ~: analz (spies evs); \
@@ -340,7 +340,7 @@
**)
(*In A's internal Note, PMS determines A and B.*)
-goal thy "!!evs. evs : tls \
+Goal "!!evs. 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);
@@ -350,7 +350,7 @@
blast_tac (claset() addSDs [Notes_Crypt_parts_spies] addSEs partsEs) 1);
val lemma = result();
-goal thy
+Goal
"!!evs. [| Notes A {|Agent B, Nonce PMS|} : set evs; \
\ Notes A' {|Agent B', Nonce PMS|} : set evs; \
\ evs : tls |] \
@@ -364,7 +364,7 @@
(*Key compromise lemma needed to prove analz_image_keys.
No collection of keys can help the spy get new private keys.*)
-goal thy
+Goal
"!!evs. evs : tls ==> \
\ ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \
\ (priK B : KK | B : bad)";
@@ -378,12 +378,12 @@
(*slightly speeds up the big simplification below*)
-goal thy "!!evs. KK <= range sessionK ==> priK B ~: KK";
+Goal "!!evs. 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 thy
+Goal
"!!evs. (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);
@@ -394,7 +394,7 @@
\ (Nonce N : analz (spies evs))";
**)
-goal thy
+Goal
"!!evs. evs : tls ==> \
\ ALL KK. KK <= range sessionK --> \
\ (Nonce N : analz (Key``KK Un (spies evs))) = \
@@ -403,7 +403,7 @@
by (ClientKeyExch_tac 7);
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac analz_image_keys_lemma));
-by (ALLGOALS (*18 seconds*)
+by (ALLGOALS (*4.5 seconds*)
(asm_simp_tac (analz_image_keys_ss
addsimps (split_ifs@pushes)
addsimps [range_sessionkeys_not_priK,
@@ -414,7 +414,7 @@
qed_spec_mp "analz_image_keys";
(*Knowing some session keys is no help in getting new nonces*)
-goal thy
+Goal
"!!evs. evs : tls ==> \
\ Nonce N : analz (insert (Key (sessionK z)) (spies evs)) = \
\ (Nonce N : analz (spies evs))";
@@ -432,7 +432,7 @@
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 thy
+Goal
"!!evs. [| Nonce PMS ~: parts (spies evs); \
\ K = sessionK((Na, Nb, PRF(PMS,NA,NB)), b); \
\ evs : tls |] \
@@ -455,14 +455,14 @@
addSEs spies_partsEs) 1));
val lemma = result();
-goal thy
+Goal
"!!evs. [| 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 thy
+Goal
"!!evs. [| Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y \
\ : parts (spies evs); evs : tls |] \
\ ==> Nonce PMS : parts (spies evs)";
@@ -473,7 +473,7 @@
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 thy
+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)";
@@ -491,7 +491,7 @@
(*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*)
-goal thy
+Goal
"!!evs. [| evs : tls; A ~: bad; B ~: bad |] \
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
\ Nonce PMS ~: analz (spies evs)";
@@ -513,7 +513,7 @@
(*If A sends ClientKeyExch to an honest B, then the MASTER SECRET
will stay secret.*)
-goal thy
+Goal
"!!evs. [| evs : tls; A ~: bad; B ~: bad |] \
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
\ Nonce (PRF(PMS,NA,NB)) ~: analz (spies evs)";
@@ -541,7 +541,7 @@
(*If A created PMS then nobody other than the Spy would send a message
using a clientK generated from that PMS.*)
-goal thy
+Goal
"!!evs. [| 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 --> \
@@ -561,7 +561,7 @@
(*If A created PMS and has not leaked her clientK to the Spy,
then nobody has.*)
-goal thy
+Goal
"!!evs. evs : tls \
\ ==> Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \
\ Notes A {|Agent B, Nonce PMS|} : set evs --> \
@@ -585,7 +585,7 @@
(*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 thy
+Goal
"!!evs. [| 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 --> \
@@ -608,7 +608,7 @@
(*If A created PMS for B, and B has not leaked his serverK to the Spy,
then nobody has.*)
-goal thy
+Goal
"!!evs. [| 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 --> \
@@ -634,7 +634,7 @@
***)
(*The mention of her name (A) in X assures A that B knows who she is.*)
-goal thy
+Goal
"!!evs. [| X = Crypt (serverK(Na,Nb,M)) \
\ (Hash{|Number SID, Nonce M, \
\ Nonce Na, Number PA, Agent A, \
@@ -659,7 +659,7 @@
val lemma = normalize_thm [RSmp] (result());
(*Final version*)
-goal thy
+Goal
"!!evs. [| X = Crypt (serverK(Na,Nb,M)) \
\ (Hash{|Number SID, Nonce M, \
\ Nonce Na, Number PA, Agent A, \
@@ -681,7 +681,7 @@
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 thy
+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 --> \
@@ -709,7 +709,7 @@
val lemma = normalize_thm [RSmp] (result());
(*Final version*)
-goal thy
+Goal
"!!evs. [| M = PRF(PMS,NA,NB); \
\ Crypt (serverK(Na,Nb,M)) Y : parts (spies evs); \
\ Notes A {|Agent B, Nonce PMS|} : set evs; \
@@ -728,7 +728,7 @@
ClientFinished, then B can then check the quoted values PA, PB, etc.
***)
-goal thy
+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 --> \
@@ -751,7 +751,7 @@
val lemma = normalize_thm [RSmp] (result());
(*Final version*)
-goal thy
+Goal
"!!evs. [| M = PRF(PMS,NA,NB); \
\ Crypt (clientK(Na,Nb,M)) Y : parts (spies evs); \
\ Notes A {|Agent B, Nonce PMS|} : set evs; \
@@ -768,7 +768,7 @@
check a CertVerify from A, then A has used the quoted
values PA, PB, etc. Even this one requires A to be uncompromised.
***)
-goal thy
+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; \
--- a/src/HOL/Auth/WooLam.ML Wed Jun 24 10:33:42 1998 +0200
+++ b/src/HOL/Auth/WooLam.ML Wed Jun 24 11:24:52 1998 +0200
@@ -21,7 +21,7 @@
(*A "possibility property": there are traces that reach the end*)
-goal thy
+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";
@@ -35,7 +35,7 @@
(**** Inductive proofs about woolam ****)
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : woolam ==> ALL A X. Says A A X ~: set evs";
+Goal "!!evs. 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 +45,7 @@
(** For reasoning about the encrypted portion of messages **)
-goal thy "!!evs. Says A' B X : set evs ==> X : analz (spies evs)";
+Goal "!!evs. Says A' B X : set evs ==> X : analz (spies evs)";
by (etac (Says_imp_spies RS analz.Inj) 1);
qed "WL4_analz_spies";
@@ -63,14 +63,14 @@
sends messages containing X! **)
(*Spy never sees another agent's shared key! (unless it's bad at start)*)
-goal thy
+Goal
"!!evs. 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 thy
+Goal
"!!evs. evs : woolam ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
by Auto_tac;
qed "Spy_analz_shrK";
@@ -86,7 +86,7 @@
(*** WL4 ***)
(*If the encrypted message appears then it originated with Alice*)
-goal thy
+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";
@@ -98,7 +98,7 @@
(*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 thy
+Goal
"!!evs. [| Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \
\ : set evs; \
\ A ~: bad; evs : woolam |] \
@@ -112,7 +112,7 @@
(*** WL5 ***)
(*Server sent WL5 only if it received the right sort of message*)
-goal thy
+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|} \
@@ -125,7 +125,7 @@
AddDs [Server_sent_WL5];
(*If the encrypted message appears then it originated with the Server!*)
-goal thy
+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";
@@ -138,7 +138,7 @@
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 thy
+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";
@@ -147,7 +147,7 @@
(*B only issues challenges in response to WL1. Not used.*)
-goal thy
+Goal
"!!evs. [| 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);
@@ -157,7 +157,7 @@
(**CANNOT be proved because A doesn't know where challenges come from...
-goal thy
+Goal
"!!evs. [| A ~: bad; B ~= Spy; evs : woolam |] \
\ ==> Crypt (shrK A) (Nonce NB) : parts (spies evs) & \
\ Says B A (Nonce NB) : set evs \
--- a/src/HOL/Auth/Yahalom.ML Wed Jun 24 10:33:42 1998 +0200
+++ b/src/HOL/Auth/Yahalom.ML Wed Jun 24 11:24:52 1998 +0200
@@ -18,7 +18,7 @@
(*A "possibility property": there are traces that reach the end*)
-goal thy
+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";
@@ -32,7 +32,7 @@
(**** Inductive proofs about yahalom ****)
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs: yahalom ==> ALL A X. Says A A X ~: set evs";
+Goal "!!evs. 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,7 +43,7 @@
(** For reasoning about the encrypted portion of messages **)
(*Lets us treat YM4 using a similar argument as for the Fake case.*)
-goal thy "!!evs. Says S A {|Crypt (shrK A) Y, X|} : set evs ==> \
+Goal "!!evs. 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,7 +52,7 @@
YM4_analz_spies RS (impOfSubs analz_subset_parts));
(*Relates to both YM4 and Oops*)
-goal thy "!!evs. Says S A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs ==> \
+Goal "!!evs. 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);
@@ -78,7 +78,7 @@
sends messages containing X! **)
(*Spy never sees another agent's shared key! (unless it's bad at start)*)
-goal thy
+Goal
"!!evs. evs : yahalom ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
@@ -86,7 +86,7 @@
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
-goal thy
+Goal
"!!evs. evs : yahalom ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
qed "Spy_analz_shrK";
@@ -97,7 +97,7 @@
(*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*)
-goal thy "!!evs. evs : yahalom ==> \
+Goal "!!evs. evs : yahalom ==> \
\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*Fake*)
@@ -115,7 +115,7 @@
(*Describes the form of K when the Server sends this message. Useful for
Oops as well as main secrecy property.*)
-goal thy
+Goal
"!!evs. [| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \
\ : set evs; \
\ evs : yahalom |] \
@@ -143,7 +143,7 @@
(** Session keys are not used to encrypt other session keys **)
-goal thy
+Goal
"!!evs. evs : yahalom ==> \
\ ALL K KK. KK <= Compl (range shrK) --> \
\ (Key K : analz (Key``KK Un (spies evs))) = \
@@ -158,7 +158,7 @@
by (spy_analz_tac 1);
qed_spec_mp "analz_image_freshK";
-goal thy
+Goal
"!!evs. [| evs : yahalom; KAB ~: range shrK |] \
\ ==> Key K : analz (insert (Key KAB) (spies evs)) = \
\ (K = KAB | Key K : analz (spies evs))";
@@ -168,7 +168,7 @@
(*** The Key K uniquely identifies the Server's message. **)
-goal thy
+Goal
"!!evs. evs : yahalom ==> \
\ EX A' B' na' nb' X'. ALL A B na nb X. \
\ Says Server A \
@@ -187,7 +187,7 @@
delrules [conjI] (*no split-up to 4 subgoals*)) 1);
val lemma = result();
-goal thy
+Goal
"!!evs. [| Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} : set evs; \
\ Says Server A' \
@@ -200,7 +200,7 @@
(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
-goal thy
+Goal
"!!evs. [| A ~: bad; B ~: bad; evs : yahalom |] \
\ ==> Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \
@@ -226,7 +226,7 @@
(*Final version*)
-goal thy
+Goal
"!!evs. [| Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \
\ Crypt (shrK B) {|Agent A, Key K|}|} \
@@ -241,7 +241,7 @@
(** Security Guarantee for A upon receiving YM3 **)
(*If the encrypted message appears then it originated with the Server*)
-goal thy
+Goal
"!!evs. [| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (spies evs); \
\ A ~: bad; evs : yahalom |] \
\ ==> Says Server A \
@@ -254,7 +254,7 @@
qed "A_trusts_YM3";
(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
-goal thy
+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 |] \
@@ -266,7 +266,7 @@
(*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 thy
+Goal
"!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (spies evs); \
\ B ~: bad; evs : yahalom |] \
\ ==> EX NA NB. Says Server A \
@@ -285,7 +285,7 @@
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 thy
+Goal
"!!evs. evs : yahalom \
\ ==> Nonce NB ~: analz (spies evs) --> \
\ Crypt K (Nonce NB) : parts (spies evs) --> \
@@ -312,14 +312,14 @@
(** Lemmas about the predicate KeyWithNonce **)
-goalw thy [KeyWithNonce_def]
+Goalw [KeyWithNonce_def]
"!!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 thy [KeyWithNonce_def]
+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'|}) \
@@ -329,7 +329,7 @@
qed "KeyWithNonce_Says";
Addsimps [KeyWithNonce_Says];
-goalw thy [KeyWithNonce_def]
+Goalw [KeyWithNonce_def]
"KeyWithNonce K NB (Notes A X # evs) = KeyWithNonce K NB evs";
by (Simp_tac 1);
qed "KeyWithNonce_Notes";
@@ -337,14 +337,14 @@
(*A fresh key cannot be associated with any nonce
(with respect to a given trace). *)
-goalw thy [KeyWithNonce_def]
+Goalw [KeyWithNonce_def]
"!!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 thy [KeyWithNonce_def]
+Goalw [KeyWithNonce_def]
"!!evs. [| Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|} \
\ : set evs; \
@@ -361,13 +361,13 @@
(*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 thy
+Goal
"!!evs. 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 thy
+Goal
"!!evs. evs : yahalom ==> \
\ (ALL KK. KK <= Compl (range shrK) --> \
\ (ALL K: KK. ~ KeyWithNonce K NB evs) --> \
@@ -402,7 +402,7 @@
(*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 thy
+Goal
"!!evs. [| Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|} \
\ : set evs; \
@@ -416,7 +416,7 @@
(*** The Nonce NB uniquely identifies B's message. ***)
-goal thy
+Goal
"!!evs. evs : yahalom ==> \
\ EX NA' A' B'. ALL NA A B. \
\ Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(spies evs) \
@@ -432,7 +432,7 @@
by (blast_tac (claset() addSEs spies_partsEs) 1);
val lemma = result();
-goal thy
+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 |] \
@@ -443,7 +443,7 @@
(*Variant useful for proving secrecy of NB: the Says... form allows
not_bad_tac to remove the assumption B' ~: bad.*)
-goal thy
+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|}|} \
@@ -459,7 +459,7 @@
(** A nonce value is never used both as NA and as NB **)
-goal thy
+Goal
"!!evs. evs : yahalom \
\ ==> Nonce NB ~: analz (spies evs) --> \
\ Crypt (shrK B') {|Agent A', Nonce NB, nb'|} : parts(spies evs) --> \
@@ -475,7 +475,7 @@
standard (result() RS mp RSN (2,rev_mp));
(*The Server sends YM3 only in response to YM2.*)
-goal thy
+Goal
"!!evs. [| Says Server A \
\ {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set evs; \
\ evs : yahalom |] \
@@ -490,7 +490,7 @@
(*A vital theorem for B, that nonce NB remains secure from the Spy.*)
-goal thy
+Goal
"!!evs. [| A ~: bad; B ~: bad; evs : yahalom |] \
\ ==> Says B Server \
\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
@@ -549,7 +549,7 @@
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 thy
+Goal
"!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Key K|}, \
\ Crypt K (Nonce NB)|} : set evs; \
\ Says B Server \
@@ -574,7 +574,7 @@
(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
-goal thy
+Goal
"!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Key K|}, \
\ Crypt K (Nonce NB)|} : set evs; \
\ Says B Server \
@@ -590,7 +590,7 @@
(*** Authenticating B to A ***)
(*The encryption in message YM2 tells us it cannot be faked.*)
-goal thy
+Goal
"!!evs. evs : yahalom \
\ ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (spies evs) --> \
\ B ~: bad --> \
@@ -601,7 +601,7 @@
bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp);
(*If the server sends YM3 then B sent YM2*)
-goal thy
+Goal
"!!evs. evs : yahalom \
\ ==> Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
\ : set evs --> \
@@ -618,7 +618,7 @@
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 thy
+Goal
"!!evs. [| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
\ : set evs; \
\ A ~: bad; B ~: bad; evs : yahalom |] \
@@ -634,7 +634,7 @@
(*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 thy
+Goal
"!!evs. evs : yahalom \
\ ==> Key K ~: analz (spies evs) --> \
\ Crypt K (Nonce NB) : parts (spies evs) --> \
@@ -659,7 +659,7 @@
(*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 thy
+Goal
"!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Key K|}, \
\ Crypt K (Nonce NB)|} : set evs; \
\ Says B Server \
--- a/src/HOL/Auth/Yahalom2.ML Wed Jun 24 10:33:42 1998 +0200
+++ b/src/HOL/Auth/Yahalom2.ML Wed Jun 24 11:24:52 1998 +0200
@@ -23,7 +23,7 @@
(*A "possibility property": there are traces that reach the end*)
-goal thy
+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";
@@ -37,7 +37,7 @@
(**** Inductive proofs about yahalom ****)
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs: yahalom ==> ALL A X. Says A A X ~: set evs";
+Goal "!!evs. 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,7 +48,7 @@
(** For reasoning about the encrypted portion of messages **)
(*Lets us treat YM4 using a similar argument as for the Fake case.*)
-goal thy "!!evs. Says S A {|NB, Crypt (shrK A) Y, X|} : set evs ==> \
+Goal "!!evs. 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,7 +57,7 @@
YM4_analz_spies RS (impOfSubs analz_subset_parts));
(*Relates to both YM4 and Oops*)
-goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B,K,NA|}, X|} : set evs ==> \
+Goal "!!evs. 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,14 +82,14 @@
sends messages containing X! **)
(*Spy never sees another agent's shared key! (unless it's bad at start)*)
-goal thy
+Goal
"!!evs. 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 thy
+Goal
"!!evs. evs : yahalom ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
by Auto_tac;
qed "Spy_analz_shrK";
@@ -100,7 +100,7 @@
(*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*)
-goal thy "!!evs. evs : yahalom ==> \
+Goal "!!evs. evs : yahalom ==> \
\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*YM4: Key K is not fresh!*)
@@ -119,7 +119,7 @@
(*Describes the form of K when the Server sends this message. Useful for
Oops as well as main secrecy property.*)
-goal thy
+Goal
"!!evs. [| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|} \
\ : set evs; \
\ evs : yahalom |] \
@@ -150,7 +150,7 @@
(** Session keys are not used to encrypt other session keys **)
-goal thy
+Goal
"!!evs. evs : yahalom ==> \
\ ALL K KK. KK <= Compl (range shrK) --> \
\ (Key K : analz (Key``KK Un (spies evs))) = \
@@ -164,7 +164,7 @@
by (spy_analz_tac 1);
qed_spec_mp "analz_image_freshK";
-goal thy
+Goal
"!!evs. [| evs : yahalom; KAB ~: range shrK |] ==> \
\ Key K : analz (insert (Key KAB) (spies evs)) = \
\ (K = KAB | Key K : analz (spies evs))";
@@ -174,7 +174,7 @@
(*** The Key K uniquely identifies the Server's message. **)
-goal thy
+Goal
"!!evs. evs : yahalom ==> \
\ EX A' B' na' nb' X'. ALL A B na nb X. \
\ Says Server A \
@@ -191,7 +191,7 @@
addss (simpset() addsimps [parts_insertI])) 1);
val lemma = result();
-goal thy
+Goal
"!!evs. [| Says Server A \
\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} : set evs; \
\ Says Server A' \
@@ -204,7 +204,7 @@
(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
-goal thy
+Goal
"!!evs. [| A ~: bad; B ~: bad; A ~= B; \
\ evs : yahalom |] \
\ ==> Says Server A \
@@ -229,7 +229,7 @@
(*Final version*)
-goal thy
+Goal
"!!evs. [| Says Server A \
\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \
\ Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \
@@ -246,7 +246,7 @@
(*If the encrypted message appears then it originated with the Server.
May now apply Spy_not_see_encrypted_key, subject to its conditions.*)
-goal thy
+Goal
"!!evs. [| Crypt (shrK A) {|Agent B, Key K, na|} \
\ : parts (spies evs); \
\ A ~: bad; evs : yahalom |] \
@@ -260,7 +260,7 @@
qed "A_trusts_YM3";
(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
-goal thy
+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 |] \
@@ -273,7 +273,7 @@
(*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 thy
+Goal
"!!evs. [| Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|} \
\ : parts (spies evs); \
\ B ~: bad; evs : yahalom |] \
@@ -293,7 +293,7 @@
(*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 thy
+Goal
"!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \
\ X|} \
\ : set evs; \
@@ -308,7 +308,7 @@
(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
-goal thy
+Goal
"!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \
\ X|} \
\ : set evs; \
@@ -323,7 +323,7 @@
(*** Authenticating B to A ***)
(*The encryption in message YM2 tells us it cannot be faked.*)
-goal thy
+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, \
@@ -337,7 +337,7 @@
(*If the server sends YM3 then B sent YM2, perhaps with a different NB*)
-goal thy
+Goal
"!!evs. [| Says Server A \
\ {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
\ : set evs; \
@@ -356,7 +356,7 @@
val lemma = result();
(*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
-goal thy
+Goal
"!!evs. [| Says S A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
\ : set evs; \
\ A ~: bad; B ~: bad; evs : yahalom |] \
@@ -373,7 +373,7 @@
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 thy
+Goal
"!!evs. evs : yahalom \
\ ==> Key K ~: analz (spies evs) --> \
\ Crypt K (Nonce NB) : parts (spies evs) --> \
@@ -398,7 +398,7 @@
(*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 thy
+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); \