--- a/src/HOL/UNITY/NSP_Bad.ML Thu Sep 10 17:29:56 1998 +0200
+++ b/src/HOL/UNITY/NSP_Bad.ML Thu Sep 10 17:30:24 1998 +0200
@@ -40,20 +40,6 @@
(**** Inductive proofs about ns_public ****)
-(*Nobody sends themselves messages*)
-Goal "Invariant Nprg {s. ALL X. Says A A X ~: set s}";
-by (rtac InvariantI 1);
-by (Force_tac 1);
-by (constrains_tac 1);
-by Auto_tac;
-qed "not_Says_to_self";
-
-(** HOW TO USE?? They don't seem to be needed!
-Addsimps [not_Says_to_self];
-AddSEs [not_Says_to_self RSN (2, rev_notE)];
-**)
-
-
(*can be used to simulate analz_mono_contra_tac
val analz_impI = read_instantiate_sg (sign_of thy)
[("P", "?Y ~: analz (spies ?evs)")] impI;
--- a/src/HOL/UNITY/NSP_Bad.thy Thu Sep 10 17:29:56 1998 +0200
+++ b/src/HOL/UNITY/NSP_Bad.thy Thu Sep 10 17:30:24 1998 +0200
@@ -22,7 +22,7 @@
Fake :: "(state*state) set"
"Fake == {(s,s').
EX B X. s' = Says Spy B X # s
- & B ~= Spy & X: synth (analz (spies s))}"
+ & X: synth (analz (spies s))}"
(*The numeric suffixes on A identify the rule*)
@@ -31,7 +31,7 @@
"NS1 == {(s1,s').
EX A1 B NA.
s' = Says A1 B (Crypt (pubK B) {|Nonce NA, Agent A1|}) # s1
- & A1 ~= B & Nonce NA ~: used s1}"
+ & Nonce NA ~: used s1}"
(*Bob responds to Alice's message with a further nonce*)
NS2 :: "(state*state) set"
@@ -39,7 +39,7 @@
EX A' A2 B NA NB.
s' = Says B A2 (Crypt (pubK A2) {|Nonce NA, Nonce NB|}) # s2
& Says A' B (Crypt (pubK B) {|Nonce NA, Agent A2|}) : set s2
- & A2 ~= B & Nonce NB ~: used s2}"
+ & Nonce NB ~: used s2}"
(*Alice proves her existence by sending NB back to Bob.*)
NS3 :: "(state*state) set"