1.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Tue Mar 13 18:35:48 2001 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Wed Mar 14 08:50:55 2001 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4  AddDs  [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert];
     1.5  
     1.6  (*A "possibility property": there are traces that reach the end*)
     1.7 -Goal "B ~= Server   \
     1.8 +Goal "B \\<noteq> Server   \
     1.9  \     ==> \\<exists>K. \\<exists>NA. \\<exists>evs \\<in> otway.          \
    1.10  \           Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
    1.11  \             \\<in> set evs";
    1.12 @@ -207,9 +207,9 @@
    1.13  (*** Attempting to prove stronger properties ***)
    1.14  
    1.15  (*Only OR1 can have caused such a part of a message to appear.
    1.16 -  The premise A ~= B prevents OR2's similar-looking cryptogram from being
    1.17 +  The premise A \\<noteq> B prevents OR2's similar-looking cryptogram from being
    1.18    picked up.  Original Otway-Rees doesn't need it.*)
    1.19 -Goal "[| A \\<notin> bad;  A ~= B;  evs \\<in> otway |]                \
    1.20 +Goal "[| A \\<notin> bad;  A \\<noteq> B;  evs \\<in> otway |]                \
    1.21  \     ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \\<in> parts (knows Spy evs) --> \
    1.22  \         Says A B {|NA, Agent A, Agent B,                  \
    1.23  \                    Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \\<in> set evs";
    1.24 @@ -220,10 +220,10 @@
    1.25  
    1.26  (*Crucial property: If the encrypted message appears, and A has used NA
    1.27    to start a run, then it originated with the Server!
    1.28 -  The premise A ~= B allows use of Crypt_imp_OR1*)
    1.29 +  The premise A \\<noteq> B allows use of Crypt_imp_OR1*)
    1.30  (*Only it is FALSE.  Somebody could make a fake message to Server
    1.31            substituting some other nonce NA' for NB.*)
    1.32 -Goal "[| A \\<notin> bad;  A ~= B;  evs \\<in> otway |]                                \
    1.33 +Goal "[| A \\<notin> bad;  A \\<noteq> B;  evs \\<in> otway |]                                \
    1.34  \     ==> Crypt (shrK A) {|NA, Key K|} \\<in> parts (knows Spy evs) -->    \
    1.35  \         Says A B {|NA, Agent A, Agent B,                        \
    1.36  \                    Crypt (shrK A) {|NA, Agent A, Agent B|}|}    \