--- a/src/HOL/Auth/Recur.ML Thu Jul 02 17:27:35 1998 +0200
+++ b/src/HOL/Auth/Recur.ML Thu Jul 02 17:48:11 1998 +0200
@@ -20,11 +20,10 @@
(*Simplest case: Alice goes directly to the server*)
-Goal
- "!!A. A ~= Server \
+Goal "A ~= Server \
\ ==> EX K NA. EX evs: recur. \
-\ Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
-\ Agent Server|} : set evs";
+\ Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
+\ Agent Server|} : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (recur.Nil RS recur.RA1 RS
(respond.One RSN (4,recur.RA3))) 2);
@@ -33,11 +32,10 @@
(*Case two: Alice, Bob and the server*)
-Goal
- "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
+Goal "[| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX K. EX NA. EX evs: recur. \
-\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
-\ Agent Server|} : set evs";
+\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
+\ Agent Server|} : set evs";
by (cut_facts_tac [Nonce_supply2, Key_supply2] 1);
by (REPEAT (eresolve_tac [exE, conjE] 1));
by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -52,11 +50,10 @@
(*Case three: Alice, Bob, Charlie and the server
TOO SLOW to run every time!
-Goal
- "!!A B. [| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |] \
+Goal "[| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |] \
\ ==> EX K. EX NA. EX evs: recur. \
-\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
-\ Agent Server|} : set evs";
+\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
+\ Agent Server|} : set evs";
by (cut_facts_tac [Nonce_supply3, Key_supply3] 1);
by (REPEAT (eresolve_tac [exE, conjE] 1));
by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -75,7 +72,7 @@
(**** Inductive proofs about recur ****)
(*Nobody sends themselves messages*)
-Goal "!!evs. evs : recur ==> ALL A X. Says A A X ~: set evs";
+Goal "evs : recur ==> ALL A X. Says A A X ~: set evs";
by (etac recur.induct 1);
by Auto_tac;
qed_spec_mp "not_Says_to_self";
@@ -84,19 +81,18 @@
-Goal "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB : parts{RB}";
+Goal "(PA,RB,KAB) : respond evs ==> Key KAB : parts{RB}";
by (etac respond.induct 1);
by (ALLGOALS Simp_tac);
qed "respond_Key_in_parts";
-Goal "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB ~: used evs";
+Goal "(PA,RB,KAB) : respond evs ==> Key KAB ~: used evs";
by (etac respond.induct 1);
by (REPEAT (assume_tac 1));
qed "respond_imp_not_used";
-Goal
- "!!evs. [| Key K : parts {RB}; (PB,RB,K') : respond evs |] \
-\ ==> Key K ~: used evs";
+Goal "[| Key K : parts {RB}; (PB,RB,K') : respond evs |] \
+\ ==> Key K ~: used evs";
by (etac rev_mp 1);
by (etac respond.induct 1);
by (auto_tac(claset() addDs [Key_not_used, respond_imp_not_used],
@@ -104,7 +100,7 @@
qed_spec_mp "Key_in_parts_respond";
(*Simple inductive reasoning about responses*)
-Goal "!!evs. (PA,RB,KAB) : respond evs ==> RB : responses evs";
+Goal "(PA,RB,KAB) : respond evs ==> RB : responses evs";
by (etac respond.induct 1);
by (REPEAT (ares_tac (respond_imp_not_used::responses.intrs) 1));
qed "respond_imp_responses";
@@ -114,8 +110,8 @@
val RA2_analz_spies = Says_imp_spies RS analz.Inj |> standard;
-Goal "!!evs. Says C' B {|Crypt K X, X', RA|} : set evs \
-\ ==> RA : analz (spies evs)";
+Goal "Says C' B {|Crypt K X, X', RA|} : set evs \
+\ ==> RA : analz (spies evs)";
by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
qed "RA4_analz_spies";
@@ -144,8 +140,7 @@
(** Spy never sees another agent's shared key! (unless it's bad at start) **)
-Goal
- "!!evs. evs : recur ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
+Goal "evs : recur ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (ALLGOALS
@@ -155,8 +150,7 @@
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
-Goal
- "!!evs. evs : recur ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
+Goal "evs : recur ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
qed "Spy_analz_shrK";
Addsimps [Spy_analz_shrK];
@@ -168,17 +162,16 @@
(** Nobody can have used non-existent keys! **)
(*The special case of H={} has the same proof*)
-Goal
- "!!evs. [| K : keysFor (parts (insert RB H)); (PB,RB,K') : respond evs |] \
-\ ==> K : range shrK | K : keysFor (parts H)";
+Goal "[| K : keysFor (parts (insert RB H)); (PB,RB,K') : respond evs |] \
+\ ==> K : range shrK | K : keysFor (parts H)";
by (etac rev_mp 1);
by (etac (respond_imp_responses RS responses.induct) 1);
by Auto_tac;
qed_spec_mp "Key_in_keysFor_parts";
-Goal "!!evs. evs : recur ==> \
-\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
+Goal "evs : recur ==> \
+\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*RA3*)
by (blast_tac (claset() addSDs [Key_in_keysFor_parts]) 2);
@@ -209,24 +202,22 @@
(*Version for "responses" relation. Handles case RA3 in the theorem below.
Note that it holds for *any* set H (not just "spies evs")
satisfying the inductive hypothesis.*)
-Goal
- "!!evs. [| RB : responses evs; \
-\ ALL K KK. KK <= Compl (range shrK) --> \
-\ (Key K : analz (Key``KK Un H)) = \
-\ (K : KK | Key K : analz H) |] \
-\ ==> ALL K KK. KK <= Compl (range shrK) --> \
-\ (Key K : analz (insert RB (Key``KK Un H))) = \
-\ (K : KK | Key K : analz (insert RB H))";
+Goal "[| RB : responses evs; \
+\ ALL K KK. KK <= Compl (range shrK) --> \
+\ (Key K : analz (Key``KK Un H)) = \
+\ (K : KK | Key K : analz H) |] \
+\ ==> ALL K KK. KK <= Compl (range shrK) --> \
+\ (Key K : analz (insert RB (Key``KK Un H))) = \
+\ (K : KK | Key K : analz (insert RB H))";
by (etac responses.induct 1);
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
qed "resp_analz_image_freshK_lemma";
(*Version for the protocol. Proof is almost trivial, thanks to the lemma.*)
-Goal
- "!!evs. evs : recur ==> \
+Goal "evs : recur ==> \
\ ALL K KK. KK <= Compl (range shrK) --> \
-\ (Key K : analz (Key``KK Un (spies evs))) = \
-\ (K : KK | Key K : analz (spies evs))";
+\ (Key K : analz (Key``KK Un (spies evs))) = \
+\ (K : KK | Key K : analz (spies evs))";
by (etac recur.induct 1);
by analz_spies_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
@@ -250,18 +241,17 @@
raw_analz_image_freshK RSN
(2, resp_analz_image_freshK_lemma) RS spec RS spec RS mp);
-Goal
- "!!evs. [| evs : recur; KAB ~: range shrK |] ==> \
-\ Key K : analz (insert (Key KAB) (spies evs)) = \
-\ (K = KAB | Key K : analz (spies evs))";
+Goal "[| evs : recur; KAB ~: range shrK |] ==> \
+\ Key K : analz (insert (Key KAB) (spies evs)) = \
+\ (K = KAB | Key K : analz (spies evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
qed "analz_insert_freshK";
(*Everything that's hashed is already in past traffic. *)
-Goal "!!evs. [| Hash {|Key(shrK A), X|} : parts (spies evs); \
-\ evs : recur; A ~: bad |] \
-\ ==> X : parts (spies evs)";
+Goal "[| Hash {|Key(shrK A), X|} : parts (spies evs); \
+\ evs : recur; A ~: bad |] \
+\ ==> X : parts (spies evs)";
by (etac rev_mp 1);
by (parts_induct_tac 1);
(*RA3 requires a further induction*)
@@ -278,11 +268,10 @@
Unicity is not used in other proofs but is desirable in its own right.
**)
-Goal
- "!!evs. [| evs : recur; A ~: bad |] \
+Goal "[| evs : recur; A ~: bad |] \
\ ==> EX B' P'. ALL B P. \
-\ Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (spies evs) \
-\ --> B=B' & P=P'";
+\ Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (spies evs) \
+\ --> B=B' & P=P'";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (etac responses.induct 3);
@@ -296,10 +285,10 @@
val lemma = result();
Goalw [HPair_def]
- "!!A.[| Hash[Key(shrK A)] {|Agent A, B,NA,P|} : parts (spies evs); \
-\ Hash[Key(shrK A)] {|Agent A, B',NA,P'|} : parts (spies evs); \
-\ evs : recur; A ~: bad |] \
-\ ==> B=B' & P=P'";
+ "[| Hash[Key(shrK A)] {|Agent A, B,NA,P|} : parts (spies evs); \
+\ Hash[Key(shrK A)] {|Agent A, B',NA,P'|} : parts (spies evs); \
+\ evs : recur; A ~: bad |] \
+\ ==> B=B' & P=P'";
by (REPEAT (eresolve_tac partsEs 1));
by (prove_unique_tac lemma 1);
qed "unique_NA";
@@ -309,8 +298,7 @@
(relations "respond" and "responses")
***)
-Goal
- "!!evs. [| RB : responses evs; evs : recur |] \
+Goal "[| RB : responses evs; evs : recur |] \
\ ==> (Key (shrK B) : analz (insert RB (spies evs))) = (B:bad)";
by (etac responses.induct 1);
by (ALLGOALS
@@ -321,13 +309,12 @@
Addsimps [shrK_in_analz_respond];
-Goal
- "!!evs. [| RB : responses evs; \
-\ ALL K KK. KK <= Compl (range shrK) --> \
-\ (Key K : analz (Key``KK Un H)) = \
-\ (K : KK | Key K : analz H) |] \
-\ ==> (Key K : analz (insert RB H)) --> \
-\ (Key K : parts{RB} | Key K : analz H)";
+Goal "[| RB : responses evs; \
+\ ALL K KK. KK <= Compl (range shrK) --> \
+\ (Key K : analz (Key``KK Un H)) = \
+\ (K : KK | Key K : analz H) |] \
+\ ==> (Key K : analz (insert RB H)) --> \
+\ (Key K : parts{RB} | Key K : analz H)";
by (etac responses.induct 1);
by (ALLGOALS
(asm_simp_tac
@@ -344,9 +331,8 @@
(*The Server does not send such messages. This theorem lets us avoid
assuming B~=Server in RA4.*)
-Goal
- "!!evs. evs : recur \
-\ ==> ALL C X Y. Says Server C {|X, Agent Server, Y|} ~: set evs";
+Goal "evs : recur \
+\ ==> ALL C X Y. Says Server C {|X, Agent Server, Y|} ~: set evs";
by (etac recur.induct 1);
by (etac (respond.induct) 5);
by Auto_tac;
@@ -355,19 +341,17 @@
(*The last key returned by respond indeed appears in a certificate*)
-Goal
- "!!K. (Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) : respond evs \
-\ ==> Crypt (shrK A) {|Key K, B, NA|} : parts {RA}";
+Goal "(Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) : respond evs \
+\ ==> Crypt (shrK A) {|Key K, B, NA|} : parts {RA}";
by (etac respond.elim 1);
by (ALLGOALS Asm_full_simp_tac);
qed "respond_certificate";
-Goal
- "!!K'. (PB,RB,KXY) : respond evs \
+Goal "!!K'. (PB,RB,KXY) : respond evs \
\ ==> EX A' B'. ALL A B N. \
-\ Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB} \
-\ --> (A'=A & B'=B) | (A'=B & B'=A)";
+\ Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB} \
+\ --> (A'=A & B'=B) | (A'=B & B'=A)";
by (etac respond.induct 1);
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [all_conj_distrib])));
(*Base case*)
@@ -385,10 +369,9 @@
by (Fast_tac 1);
val lemma = result();
-Goal
- "!!RB. [| Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB}; \
-\ Crypt (shrK A') {|Key K, Agent B', N'|} : parts {RB}; \
-\ (PB,RB,KXY) : respond evs |] \
+Goal "[| Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB}; \
+\ Crypt (shrK A') {|Key K, Agent B', N'|} : parts {RB}; \
+\ (PB,RB,KXY) : respond evs |] \
\ ==> (A'=A & B'=B) | (A'=B & B'=A)";
by (prove_unique_tac lemma 1);
qed "unique_session_keys";
@@ -398,11 +381,10 @@
Does not in itself guarantee security: an attack could violate
the premises, e.g. by having A=Spy **)
-Goal
- "!!evs. [| (PB,RB,KAB) : respond evs; evs : recur |] \
-\ ==> ALL A A' N. A ~: bad & A' ~: bad --> \
-\ Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} --> \
-\ Key K ~: analz (insert RB (spies evs))";
+Goal "[| (PB,RB,KAB) : respond evs; evs : recur |] \
+\ ==> ALL A A' N. A ~: bad & A' ~: bad --> \
+\ Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} --> \
+\ Key K ~: analz (insert RB (spies evs))";
by (etac respond.induct 1);
by (forward_tac [respond_imp_responses] 2);
by (forward_tac [respond_imp_not_used] 2);
@@ -429,10 +411,9 @@
qed_spec_mp "respond_Spy_not_see_session_key";
-Goal
- "!!evs. [| Crypt (shrK A) {|Key K, Agent A', N|} : parts (spies evs); \
-\ A ~: bad; A' ~: bad; evs : recur |] \
-\ ==> Key K ~: analz (spies evs)";
+Goal "[| Crypt (shrK A) {|Key K, Agent A', N|} : parts (spies evs); \
+\ A ~: bad; A' ~: bad; evs : recur |] \
+\ ==> Key K ~: analz (spies evs)";
by (etac rev_mp 1);
by (etac recur.induct 1);
by analz_spies_tac;
@@ -463,10 +444,9 @@
(**** Authenticity properties for Agents ****)
(*The response never contains Hashes*)
-Goal
- "!!evs. [| Hash {|Key (shrK B), M|} : parts (insert RB H); \
-\ (PB,RB,K) : respond evs |] \
-\ ==> Hash {|Key (shrK B), M|} : parts H";
+Goal "[| Hash {|Key (shrK B), M|} : parts (insert RB H); \
+\ (PB,RB,K) : respond evs |] \
+\ ==> Hash {|Key (shrK B), M|} : parts H";
by (etac rev_mp 1);
by (etac (respond_imp_responses RS responses.induct) 1);
by Auto_tac;
@@ -477,9 +457,9 @@
it can say nothing about how recent A's message is. It might later be
used to prove B's presence to A at the run's conclusion.*)
Goalw [HPair_def]
- "!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} : parts(spies evs); \
-\ A ~: bad; evs : recur |] \
-\ ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) : set evs";
+ "[| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} : parts(spies evs); \
+\ A ~: bad; evs : recur |] \
+\ ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) : set evs";
by (etac rev_mp 1);
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
@@ -493,11 +473,10 @@
(*Certificates can only originate with the Server.*)
-Goal
- "!!evs. [| Crypt (shrK A) Y : parts (spies evs); \
-\ A ~: bad; evs : recur |] \
-\ ==> EX C RC. Says Server C RC : set evs & \
-\ Crypt (shrK A) Y : parts {RC}";
+Goal "[| Crypt (shrK A) Y : parts (spies evs); \
+\ A ~: bad; evs : recur |] \
+\ ==> EX C RC. Says Server C RC : set evs & \
+\ Crypt (shrK A) Y : parts {RC}";
by (etac rev_mp 1);
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);