src/HOL/Auth/NS_Shared.ML

 AddDs [impOfSubs analz_subset_parts];
 AddDs [impOfSubs Fake_parts_insert];
 
 
 (*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";
 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);
 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";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS 

 by possibility_tac;
 
 (**** 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";
 Addsimps [not_Says_to_self];
 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);
 qed "Oops_parts_spies";
 

 
 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY
     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";
 Addsimps [Spy_analz_shrK];
 
 AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
 	Spy_analz_shrK RSN (2, rev_iffD1)];
 
 
 (*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*)
 by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
 (*NS2, NS4, NS5*)

 
 
 (** 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 &                           \
 \            X = (Crypt (shrK B) {|Key K, Agent A|}) &   \
 \            K' = shrK A";

 by Auto_tac;
 qed "Says_Server_message_form";
 
 
 (*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|})    \
 \               : set evs";
 by (etac rev_mp 1);
 by (parts_induct_tac 1);
 by (Blast_tac 1);
 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|})";
 by (blast_tac (claset() addSDs [A_trusts_NS2, Says_Server_message_form]) 1);
 qed "cert_A_form";
 
 
 (*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 |]                                             \
 \        ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|}))   \
 \            | X : analz (spies evs)";

 
 
 (*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)";
 by (parts_induct_tac 1);
 (*Fake*)

 
 
 (** 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))) =  \
 \            (K : KK | Key K : analz (spies evs))";
 by (etac ns_shared.induct 1);

 (*Fake*) 
 by (spy_analz_tac 1);
 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))";
 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
 qed "analz_insert_freshK";
 
 
 (** 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 \
 \       -->         A=A' & NA=NA' & B=B' & X=X'";
 by (etac ns_shared.induct 1);

 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
 by (Blast_tac 1);
 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'                                              \
 \             (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) : set evs; \
 \           evs : ns_shared |] ==> A=A' & NA=NA' & B=B' & X = X'";

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

 by (blast_tac (claset() addDs [unique_session_keys]) 1);
 val lemma = result() RS mp RS mp RSN(2,rev_notE);
 
 
 (*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;      \
 \           A ~: bad;  B ~: bad;  evs : ns_shared                \
 \        |] ==> Key K ~: analz (spies evs)";

 
 A_trusts_NS2 RS Spy_not_see_encrypted_key;
 
 
 (*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                                     \
 \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
 \                                Crypt (shrK B) {|Key K, Agent A|}|})  \

 by (parts_induct_tac 1);
 by (ALLGOALS Blast_tac);
 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;                                             \
 \           Key K ~: analz (spies evs);                               \
 \           evs : ns_shared |]                  \

 by (blast_tac (claset() addDs [B_trusts_NS3, unique_session_keys]) 1);
 qed "A_trusts_NS4_lemma";
 
 
 (*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;           \
 \           A ~: bad;  B ~: bad;  evs : ns_shared |]                  \
 \        ==> Says B A (Crypt K (Nonce NB)) : set evs";

 
 
 (*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;                                              \
 \           Key K ~: analz (spies evs);                               \
 \           evs : ns_shared |]                              \

 by (ALLGOALS Clarify_tac);
 by (blast_tac (claset() addDs [unique_session_keys]) 1);
 qed "NS4_implies_NS3";
 
 
-goal thy
+Goal
  "!!evs. [| B ~: bad;  evs : ns_shared |]                              \
 \        ==> Key K ~: analz (spies evs) -->                            \
 \            Says Server A                                             \
 \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
 \                                Crypt (shrK B) {|Key K, Agent A|}|})  \

 by (blast_tac (claset() addDs [A_trusts_NS2, unique_session_keys]) 1);
 qed_spec_mp "B_trusts_NS5_lemma";
 
 
 (*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);   \
 \           ALL NA NB. Notes Spy {|NA, NB, Key K|} ~: set evs;       \
 \           A ~: bad;  B ~: bad;  evs : ns_shared |]                 \