# HG changeset patch
# User paulson
# Date 859282981 -3600
# Node ID dee1c7f1f576fe6f57b89cd7918136b7ac2ecc7a
# Parent  148829646a51a22f3b334fb2d053ebdad324f8b3
Trivial renamings (for consistency with CSFW papers)

diff -r 148829646a51 -r dee1c7f1f576 src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Tue Mar 25 10:41:44 1997 +0100
+++ b/src/HOL/Auth/OtwayRees.ML	Tue Mar 25 10:43:01 1997 +0100
@@ -57,7 +57,7 @@
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
 qed "OR2_analz_sees_Spy";
 
-goal thy "!!evs. Says S B {|N, X, Crypt (shrK B) X'|} : set_of_list evs \
+goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set_of_list evs \
 \                ==> X : analz (sees lost Spy evs)";
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
 qed "OR4_analz_sees_Spy";
@@ -487,7 +487,7 @@
   has sent the correct message.*)
 goal thy 
  "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost;               \
-\           Says S B {|NA, X, Crypt (shrK B) {|NB, Key K|}|}       \
+\           Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|}      \
 \            : set_of_list evs;                                    \
 \           Says B Server {|NA, Agent A, Agent B, X',              \
 \                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
diff -r 148829646a51 -r dee1c7f1f576 src/HOL/Auth/OtwayRees.thy
--- a/src/HOL/Auth/OtwayRees.thy	Tue Mar 25 10:41:44 1997 +0100
+++ b/src/HOL/Auth/OtwayRees.thy	Tue Mar 25 10:43:01 1997 +0100
@@ -66,7 +66,7 @@
                              Crypt (shrK B)
                                    {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
                : set_of_list evs;
-             Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
+             Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
                : set_of_list evs |]
           ==> Says B A {|Nonce NA, X|} # evs : otway lost"
 
diff -r 148829646a51 -r dee1c7f1f576 src/HOL/Auth/OtwayRees_AN.ML
--- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Mar 25 10:41:44 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Tue Mar 25 10:43:01 1997 +0100
@@ -52,7 +52,7 @@
 
 (** For reasoning about the encrypted portion of messages **)
 
-goal thy "!!evs. Says S B {|X, Crypt(shrK B) X'|} : set_of_list evs ==> \
+goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set_of_list evs ==> \
 \                X : analz (sees lost Spy evs)";
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
 qed "OR4_analz_sees_Spy";
@@ -353,7 +353,7 @@
   has sent the correct message in round 3.*)
 goal thy 
  "!!evs. [| B ~: lost;  evs : otway lost;                                   \
-\           Says S B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}  \
+\           Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
 \            : set_of_list evs |]                                           \
 \        ==> EX NA. Says Server B                                           \
 \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
diff -r 148829646a51 -r dee1c7f1f576 src/HOL/Auth/OtwayRees_AN.thy
--- a/src/HOL/Auth/OtwayRees_AN.thy	Tue Mar 25 10:41:44 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.thy	Tue Mar 25 10:43:01 1997 +0100
@@ -58,7 +58,7 @@
     OR4  "[| evs: otway lost;  A ~= B;
              Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
                : set_of_list evs;
-             Says S B {|X, Crypt(shrK B){|Nonce NB, Agent A, Agent B, Key K|}|}
+             Says S' B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
                : set_of_list evs |]
           ==> Says B A X # evs : otway lost"
 
diff -r 148829646a51 -r dee1c7f1f576 src/HOL/Auth/OtwayRees_Bad.ML
--- a/src/HOL/Auth/OtwayRees_Bad.ML	Tue Mar 25 10:41:44 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML	Tue Mar 25 10:43:01 1997 +0100
@@ -51,7 +51,7 @@
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
 qed "OR2_analz_sees_Spy";
 
-goal thy "!!evs. Says S B {|N, X, Crypt (shrK B) X'|} : set_of_list evs ==> \
+goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set_of_list evs ==> \
 \                X : analz (sees lost Spy evs)";
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
 qed "OR4_analz_sees_Spy";
diff -r 148829646a51 -r dee1c7f1f576 src/HOL/Auth/OtwayRees_Bad.thy
--- a/src/HOL/Auth/OtwayRees_Bad.thy	Tue Mar 25 10:41:44 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.thy	Tue Mar 25 10:43:01 1997 +0100
@@ -63,7 +63,7 @@
     OR4  "[| evs: otway;  A ~= B;
              Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
                : set_of_list evs;
-             Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
+             Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
                : set_of_list evs |]
           ==> Says B A {|Nonce NA, X|} # evs : otway"