wneuper/isa: comparison src/HOL/Auth/OtwayRees

equal deleted inserted replaced

-:881222d48777
+:bb01189f0565
 AddDs  [Says_imp_knows_Spy RS parts.Inj, parts.Body];
 AddDs  [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert];
 (*A "possibility property": there are traces that reach the end*)
-Goal "B ~= Server   \
+Goal "B \\<noteq> Server   \
 \     ==> \\<exists>K. \\<exists>NA. \\<exists>evs \\<in> otway.                                      \
 \          Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
 \            \\<in> set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (otway.Nil RS
 (****
 The following is to prove theorems of the form
-Key K : analz (insert (Key KAB) (knows Spy evs)) ==>
+Key K \\<in> analz (insert (Key KAB) (knows Spy evs)) ==>
-Key K : analz (knows Spy evs)
+Key K \\<in> analz (knows Spy evs)
 A more general formula must be proved inductively.
 ****)
 (**** Authenticity properties relating to NA ****)
 (*If the encrypted message appears then it originated with the Server!*)
-Goal "[| A \\<notin> bad;  A ~= B;  evs \\<in> otway |]                 \
+Goal "[| A \\<notin> bad;  A \\<noteq> B;  evs \\<in> otway |]                 \
 \     ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} \\<in> parts (knows Spy evs) \
 \      --> (\\<exists>NB. Says Server B                                          \
 \                   {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
 \                     Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
 \                   \\<in> set evs)";
 (*Corollary: if A receives B's OR4 message then it originated with the Server.
 Freshness may be inferred from nonce NA.*)
 Goal "[| Gets A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
 \         \\<in> set evs;                                                 \
-\        A \\<notin> bad;  A ~= B;  evs \\<in> otway |]                          \
+\        A \\<notin> bad;  A \\<noteq> B;  evs \\<in> otway |]                          \
 \     ==> \\<exists>NB. Says Server B                                       \
 \                 {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
 \                   Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
 \                \\<in> set evs";
 by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1);
 (*A's guarantee.  The Oops premise quantifies over NB because A cannot know
 what it is.*)
 Goal "[| Gets A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
 \         \\<in> set evs;                                                 \
 \        ALL NB. Notes Spy {|NA, NB, Key K|} \\<notin> set evs;             \
-\        A \\<notin> bad;  B \\<notin> bad;  A ~= B;  evs \\<in> otway |]               \
+\        A \\<notin> bad;  B \\<notin> bad;  A \\<noteq> B;  evs \\<in> otway |]               \
 \     ==> Key K \\<notin> analz (knows Spy evs)";
 by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1);
 qed "A_gets_good_key";
 (**** Authenticity properties relating to NB ****)
 (*If the encrypted message appears then it originated with the Server!*)
-Goal "[| B \\<notin> bad;  A ~= B;  evs \\<in> otway |]                              \
+Goal "[| B \\<notin> bad;  A \\<noteq> B;  evs \\<in> otway |]                              \
 \ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} \\<in> parts (knows Spy evs) \
 \     --> (\\<exists>NA. Says Server B                                          \
 \                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
 \                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
 \                  \\<in> set evs)";
 (*Guarantee for B: if it gets a well-formed certificate then the Server
 has sent the correct message in round 3.*)
 Goal "[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
 \          \\<in> set evs;                                                    \
-\        B \\<notin> bad;  A ~= B;  evs \\<in> otway |]                              \
+\        B \\<notin> bad;  A \\<noteq> B;  evs \\<in> otway |]                              \
 \     ==> \\<exists>NA. Says Server B                                           \
 \                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
 \                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
 \                  \\<in> set evs";
 by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1);
 (*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*)
 Goal "[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
 \         \\<in> set evs;                                                     \
 \        ALL NA. Notes Spy {|NA, NB, Key K|} \\<notin> set evs;                 \
-\        A \\<notin> bad;  B \\<notin> bad;  A ~= B;  evs \\<in> otway |]                   \
+\        A \\<notin> bad;  B \\<notin> bad;  A \\<noteq> B;  evs \\<in> otway |]                   \
 \     ==> Key K \\<notin> analz (knows Spy evs)";
 by (blast_tac (claset() addDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1);
 qed "B_gets_good_key";

changeset 11204	bb01189f0565
parent 11185	1b737b4c2108
child 11230	756c5034f08b