# HG changeset patch
# User paulson
# Date 849865755 -3600
# Node ID d6a56ff0d94ed21c37ac22cb07ec200653a9859c
# Parent  3eea6b72bb4fe106d911ee54e505b64e968a42d6
Minor renamings

diff -r 3eea6b72bb4f -r d6a56ff0d94e src/HOL/Auth/OtwayRees_AN.ML
--- a/src/HOL/Auth/OtwayRees_AN.ML	Fri Dec 06 10:47:10 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Dec 06 10:49:15 1996 +0100
@@ -18,10 +18,10 @@
 HOL_quantifiers := false;
 
 
-(*Weak liveness: there are traces that reach the end*)
+(*A "possibility property": there are traces that reach the end*)
 goal thy 
- "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
-\        ==> EX K. EX NA. EX evs: otway lost.          \
+ "!!A B. [| A ~= B; A ~= Server; B ~= Server |]                               \
+\        ==> EX K. EX NA. EX evs: otway lost.                                 \
 \             Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
 \             : set_of_list evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -120,8 +120,8 @@
 (*** Future keys can't be seen or used! ***)
 
 (*Nobody can have SEEN keys that will be generated in the future. *)
-goal thy "!!evs. evs : otway lost ==> \
-\                length evs <= length evs' --> \
+goal thy "!!evs. evs : otway lost ==>             \
+\                length evs <= length evs' -->    \
 \                Key (newK evs') ~: parts (sees lost Spy evs)";
 by (parts_induct_tac 1);
 by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
@@ -147,7 +147,7 @@
 
 (*Nobody can have USED keys that will be generated in the future.
   ...very like new_keys_not_seen*)
-goal thy "!!evs. evs : otway lost ==> \
+goal thy "!!evs. evs : otway lost ==>          \
 \                length evs <= length evs' --> \
 \                newK evs' ~: keysFor (parts (sees lost Spy evs))";
 by (parts_induct_tac 1);
@@ -176,11 +176,11 @@
 (*Describes the form of K and NA when the Server sends this message.*)
 goal thy 
  "!!evs. [| Says Server B \
-\           {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                    \
+\           {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                     \
 \             Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs; \
-\           evs : otway lost |]                                        \
-\        ==> (EX evt: otway lost. K = Key(newK evt)) &                  \
-\            (EX i. NA = Nonce i) &                  \
+\           evs : otway lost |]                                               \
+\        ==> (EX evt: otway lost. K = Key(newK evt)) & \
+\            (EX i. NA = Nonce i) &                    \
 \            (EX j. NB = Nonce j)";
 by (etac rev_mp 1);
 by (etac otway.induct 1);
@@ -211,7 +211,7 @@
 
 (*The equality makes the induction hypothesis easier to apply*)
 goal thy  
- "!!evs. evs : otway lost ==> \
+ "!!evs. evs : otway lost ==>                                         \
 \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
 \           (K : newK``E | Key K : analz (sees lost Spy evs))";
 by (etac otway.induct 1);
@@ -231,7 +231,7 @@
 
 
 goal thy
- "!!evs. evs : otway lost ==>                               \
+ "!!evs. evs : otway lost ==>                                          \
 \        Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
 \        (K = newK evt | Key K : analz (sees lost Spy evs))";
 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
@@ -243,10 +243,10 @@
 (*** The Key K uniquely identifies the Server's  message. **)
 
 goal thy 
- "!!evs. evs : otway lost ==>                      \
+ "!!evs. evs : otway lost ==>                              \
 \      EX A' B' NA' NB'. ALL A B NA NB.                    \
 \       Says Server B \
-\         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                    \
+\         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                     \
 \           Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs  \
 \       --> A=A' & B=B' & NA=NA' & NB=NB'";
 by (etac otway.induct 1);
@@ -291,7 +291,7 @@
  "!!evs. [| A ~: lost;  evs : otway lost |]                 \
 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}        \
 \      : parts (sees lost Spy evs)                          \
-\     --> (EX NB. Says Server B                                     \
+\     --> (EX NB. Says Server B                                          \
 \                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
 \                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
 \                  : set_of_list evs)";
@@ -318,7 +318,7 @@
 by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
                       addEs  partsEs
                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
-qed "A_trust_OR4";
+qed "A_trusts_OR4";
 
 
 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
@@ -407,4 +407,4 @@
 by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
                       addEs  partsEs
                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
-qed "B_trust_OR3";
+qed "B_trusts_OR3";