# HG changeset patch
# User paulson
# Date 872161044 -7200
# Node ID 5f6ab7fbd53b83124b77db1516e434eeb1a37076
# Parent  282ffdc918844b494c201f9341f3e17563ddd6ee
Simplified the statement of A_trusts_NS2

diff -r 282ffdc91884 -r 5f6ab7fbd53b src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Thu Aug 21 12:56:29 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.ML	Thu Aug 21 12:57:24 1997 +0200
@@ -126,18 +126,14 @@
 
 (*If the encrypted message appears then it originated with the Server*)
 goal thy
- "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|}                   \
-\            : parts (sees Spy evs);                              \
-\           A ~: lost;  evs : ns_shared |]                        \
-\         ==> X = (Crypt (shrK B) {|Key K, Agent A|}) &                \
-\             Says Server A                                            \
-\              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
-\                                Crypt (shrK B) {|Key K, Agent A|}|})  \
-\             : set evs";
+ "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|}                    \
+\            : parts (sees Spy evs);                                    \
+\           A ~: lost;  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 (Fake_parts_insert_tac 1);
-by (Auto_tac());
 qed "A_trusts_NS2";
 
 
@@ -146,15 +142,15 @@
   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 |]                   \
+\              : set evs;                                                  \
+\           evs : ns_shared |]                                             \
 \        ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|}))   \
 \            | X : analz (sees Spy evs)";
 by (case_tac "A : lost" 1);
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
                       addss (!simpset)) 1);
 by (forward_tac [Says_imp_sees_Spy RS parts.Inj] 1);
-by (blast_tac (!claset addEs  partsEs
-                      addSDs [A_trusts_NS2, Says_Server_message_form]) 1);
+by (blast_tac (!claset addSDs [A_trusts_NS2, Says_Server_message_form]) 1);
 qed "Says_S_message_form";
 
 
@@ -304,7 +300,7 @@
 
 (**** Guarantees available at various stages of protocol ***)
 
-A_trusts_NS2 RS conjunct2 RS Spy_not_see_encrypted_key;
+A_trusts_NS2 RS Spy_not_see_encrypted_key;
 
 
 (*If the encrypted message appears then it originated with the Server*)