# HG changeset patch
# User paulson
# Date 916740903 -3600
# Node ID 5cb525437aabf55d19befc6bb703fe7d2e269254
# Parent  166b3353aad5735b637c852f92aa378ccd8f679b
a simplification by G Bella

diff -r 166b3353aad5 -r 5cb525437aab src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Mon Jan 18 21:12:42 1999 +0100
+++ b/src/HOL/Auth/NS_Shared.ML	Tue Jan 19 11:15:03 1999 +0100
@@ -358,12 +358,9 @@
 \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
 \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
 \             : set evs -->                                            \
-\            Says B A (Crypt K (Nonce NB))  : set evs -->              \
 \            Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs) -->    \
 \            Says A B (Crypt K {|Nonce NB, Nonce NB|}) : set evs";
 by (parts_induct_tac 1);
-(*NS4*)
-by (Blast_tac 4);
 (*NS3*)
 by (blast_tac (claset() addSDs [cert_A_form]) 3);
 (*NS2*)
@@ -380,7 +377,6 @@
 
 (*Very strong Oops condition reveals protocol's weakness*)
 Goal "[| 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 |]                 \