src/HOL/Auth/OtwayRees_AN.ML

 
 proof_timing:=true;
 HOL_quantifiers := false;
 
 
-(*Weak liveness: 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 "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.                                 \
 \             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));
 by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
 by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));

 
 
 (*** 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]
 				    addDs [impOfSubs analz_subset_parts,
                                            impOfSubs parts_insert_subset_Un,

 qed "Says_imp_old_keys";
 
 
 (*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);
 (*OR1 and OR3*)
 by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));

 (*** Proofs involving analz ***)
 
 (*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);
 by (ALLGOALS (fast_tac (!claset addss (!simpset))));
 qed "Says_Server_message_form";

 
 (** Session keys are not used to encrypt other session keys **)
 
 (*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);
 by analz_Fake_tac;
 by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));

 by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
 qed_spec_mp "analz_image_newK";
 
 
 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, 
                                    insert_Key_singleton]) 1);
 by (Fast_tac 1);

 
 
 (*** 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);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
 by (Step_tac 1);

 (*If the encrypted message appears then it originated with the Server!*)
 goal thy 
  "!!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)";
 by (parts_induct_tac 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));

 \                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
 \                   : set_of_list evs";
 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
     Does not in itself guarantee security: an attack could violate 
     the premises, e.g. by having A=Spy **)

 \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
 \                     : set_of_list evs";
 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";