src/HOL/Auth/NS_Shared.ML

 val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy;
 
 
 (*A "possibility property": there are traces that reach the end*)
 goal thy 
- "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
+ "!!A B. [| A ~= B; A ~= Server; B ~= Server |]       \
 \        ==> EX N K. EX evs: ns_shared lost.          \
 \               Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS 
           ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2);

 (*Monotonicity*)
 goal thy "!!evs. lost' <= lost ==> ns_shared lost' <= ns_shared lost";
 by (rtac subsetI 1);
 by (etac ns_shared.induct 1);
 by (REPEAT_FIRST
-    (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
+    (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
                               :: ns_shared.intrs))));
 qed "ns_shared_mono";
 
 
 (*Nobody sends themselves messages*)

 (** 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 
  "!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) \
-\             : set evs;                              \
+\             : set evs;                                      \
 \           evs : ns_shared lost |]                           \
 \        ==> K ~: range shrK &                                \
 \            X = (Crypt (shrK B) {|Key K, Agent A|}) &        \
 \            K' = shrK A";
 by (etac rev_mp 1);

 (*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 
  "!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})      \
-\            : set evs;  evs : ns_shared lost |]                   \
+\            : set evs;          evs : ns_shared lost |]                   \
 \        ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|}))   \
 \            | X : analz (sees lost Spy evs)";
 by (case_tac "A : lost" 1);
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]
                       addss (!simpset)) 1);

 
 (*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 
- "!!evs. [| evs : ns_shared lost;  Kab ~: range shrK |] ==> \
-\        (Crypt KAB X) : parts (sees lost Spy evs) & \
-\        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
+ "!!evs. [| evs : ns_shared lost;  Kab ~: range shrK |] ==>  \
+\           (Crypt KAB X) : parts (sees lost Spy evs) &      \
+\           Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
 by parts_induct_tac;
 (*Deals with Faked messages*)
 by (blast_tac (!claset addSEs partsEs
                        addDs [impOfSubs parts_insert_subset_Un]) 1);
 (*Base, NS4 and NS5*)

 
 (** Session keys are not used to encrypt other session keys **)
 
 (*The equality makes the induction hypothesis easier to apply*)
 goal thy  
- "!!evs. evs : ns_shared lost ==> \
-\  ALL K KK. KK <= Compl (range shrK) -->                      \
-\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
+ "!!evs. evs : ns_shared lost ==>                                \
+\  ALL K KK. KK <= Compl (range shrK) -->                        \
+\            (Key K : analz (Key``KK Un (sees lost Spy evs))) =  \
 \            (K : KK | Key K : analz (sees lost Spy evs))";
 by (etac ns_shared.induct 1);
 by analz_sees_tac;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
 by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));

 
 goal thy 
  "!!evs. evs : ns_shared lost ==>                                        \
 \      EX A' NA' B' X'. ALL A NA B X.                                    \
 \       Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})         \
-\       : set evs --> A=A' & NA=NA' & B=B' & X=X'";
+\       : set evs -->         A=A' & NA=NA' & B=B' & X=X'";
 by (etac ns_shared.induct 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
 by (Step_tac 1);
 (*NS3*)
 by (ex_strip_tac 2);

 
 (*In messages of this form, the session key uniquely identifies the rest*)
 goal thy 
  "!!evs. [| Says Server A                                    \
 \             (Crypt (shrK A) {|NA, Agent B, Key K, X|})     \
-\                  : set evs;                        \ 
+\                  : set evs;                                \ 
 \           Says Server A'                                   \
 \             (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) \
-\                  : set evs;                        \
+\                  : set evs;                                \
 \           evs : ns_shared lost |] ==> A=A' & NA=NA' & B=B' & X = X'";
 by (prove_unique_tac lemma 1);
 qed "unique_session_keys";
 
 

 goal thy 
  "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_shared lost |]            \
 \        ==> Says Server A                                             \
 \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
 \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
-\             : set evs -->                                    \
-\        (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs) --> \
+\             : set evs -->                                            \
+\        (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs) -->         \
 \        Key K ~: analz (sees lost Spy evs)";
 by (etac ns_shared.induct 1);
 by analz_sees_tac;
 by (ALLGOALS 
     (asm_simp_tac 

 
 
 (*Final version: Server's message in the most abstract form*)
 goal thy 
  "!!evs. [| Says Server A                                               \
-\            (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;    \
-\           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs);  \
+\            (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;            \
+\           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs);          \
 \           A ~: lost;  B ~: lost;  evs : ns_shared lost                \
 \        |] ==> Key K ~: analz (sees lost Spy evs)";
 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
 by (blast_tac (!claset addSDs [lemma]) 1);
 qed "Spy_not_see_encrypted_key";
 
 
 goal thy 
  "!!evs. [| C ~: {A,B,Server};                                          \
 \           Says Server A                                               \
-\            (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;    \
-\           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs);  \
+\            (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;            \
+\           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs);          \
 \           A ~: lost;  B ~: lost;  evs : ns_shared lost |]             \
 \        ==> Key K ~: analz (sees lost C evs)";
 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));

 by (ALLGOALS Blast_tac);
 qed "B_trusts_NS3";
 
 
 goal thy
- "!!evs. [| B ~: lost;  evs : ns_shared lost |]            \
-\        ==> Key K ~: analz (sees lost Spy evs) -->             \
+ "!!evs. [| B ~: lost;  evs : ns_shared lost |]                        \
+\        ==> Key K ~: analz (sees lost Spy evs) -->                    \
 \            Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
-\            : set evs --> \
-\            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->            \
+\            : set evs -->                                             \
+\            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->        \
 \            Says B A (Crypt K (Nonce NB)) : set evs";
 by (etac ns_shared.induct 1);
 by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
 by (dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5);
 by (forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8);

 val lemma = result();
 
 goal thy
  "!!evs. [| Crypt K (Nonce NB) : parts (sees lost Spy evs);           \
 \           Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
-\           : set evs;                                        \
-\           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs;  \
+\           : set evs;                                                \
+\           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs;          \
 \           A ~: lost;  B ~: lost;  evs : ns_shared lost |]           \
 \        ==> Says B A (Crypt K (Nonce NB)) : set evs";
 by (blast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
                        addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
 qed "A_trusts_NS4";